etc/settings
changeset 79951 84f2d481d6d7
parent 79740 ea1913c953ef
child 79991 99511fa536a1
--- a/etc/settings	Thu Mar 21 12:47:51 2024 +0100
+++ b/etc/settings	Thu Mar 21 14:19:05 2024 +0100
@@ -185,7 +185,5 @@
 ISABELLE_GNUPLOT="gnuplot"
 ISABELLE_FONTFORGE="fontforge"
 
-#ISABELLE_MLTON="/usr/bin/mlton"
-#ISABELLE_MLTON_OPTIONS="-pi-style npi"
 #ISABELLE_SMLNJ="/usr/bin/sml"
 #ISABELLE_SWIPL="/usr/bin/swipl"