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"