diff options
Diffstat (limited to 'sci-mathematics/twelf/files/twelf-1.7.1-mlton-20180207.patch')
| -rw-r--r-- | sci-mathematics/twelf/files/twelf-1.7.1-mlton-20180207.patch | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/sci-mathematics/twelf/files/twelf-1.7.1-mlton-20180207.patch b/sci-mathematics/twelf/files/twelf-1.7.1-mlton-20180207.patch new file mode 100644 index 000000000000..823d3e37a8d8 --- /dev/null +++ b/sci-mathematics/twelf/files/twelf-1.7.1-mlton-20180207.patch @@ -0,0 +1,11 @@ +--- twelf-orig/Makefile 2018-03-06 23:30:35.055598250 +1100 ++++ twelf/Makefile 2018-03-06 23:24:44.403762472 +1100 +@@ -11,7 +11,7 @@ + polyml = poly + smlnj = sml + oldnj = sml +-mlton = mlton -default-ann 'nonexhaustiveMatch ignore' ++mlton = mlton -disable-ann nonexhaustiveMatch + make = make + + twelfdir = `pwd` |