1 files changed, 0 insertions, 11 deletions
diff --git a/lang/mlton/files/patch-runtime-cenv.h b/lang/mlton/files/patch-runtime-cenv.h
deleted file mode 100644
index 3d3ebd4d3cd2..000000000000
--- a/lang/mlton/files/patch-runtime-cenv.h
+++ /dev/null
@@ -1,11 +0,0 @@
---- runtime/cenv.h.orig	2008-04-27 10:56:05.000000000 +1000
-+++ runtime/cenv.h	2008-04-27 10:56:20.000000000 +1000
-@@ -116,7 +116,7 @@
- #error unknown platform arch
- #endif
- 
--#include "gmp.h"
-+#include "/usr/local/include/gmp.h"
- 
- COMPILE_TIME_ASSERT(sizeof_uintptr_t__is__sizeof_voidStar, 
-                     sizeof(uintptr_t) == sizeof(void*));