etc/settings
changeset 62354 fdd6989cc8a0
parent 62233 dbc39c04a34a
child 62559 83e815849a91
--- a/etc/settings	Wed Feb 17 21:08:18 2016 +0100
+++ b/etc/settings	Wed Feb 17 23:06:24 2016 +0100
@@ -129,17 +129,9 @@
 
 
 ###
-### Misc old-style settings
+### Misc settings
 ###
 
-# Standard ML of New Jersey (slow!)
-#ML_SYSTEM=smlnj-110
-#ML_HOME="/usr/local/smlnj/bin"
-#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
-#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-#SMLNJ_CYGWIN_RUNTIME=1
-
-# Misc programming languages
 #ISABELLE_GHC="/usr/bin/ghc"
 #ISABELLE_OCAML="/usr/bin/ocaml"
 #ISABELLE_SWIPL="/usr/bin/swipl"