# HG changeset patch
# User wenzelm
# Date 1194548877 -3600
# Node ID 297e2520ee824da2c94bd54960cc1e24a73b06d8
# Parent  7f2e3292e3dd2cce33b4ac8ee35a6ab345133213
tuned comments;

diff -r 7f2e3292e3dd -r 297e2520ee82 etc/settings
--- a/etc/settings	Thu Nov 08 14:51:31 2007 +0100
+++ b/etc/settings	Thu Nov 08 20:07:57 2007 +0100
@@ -30,35 +30,40 @@
 ML_OPTIONS="-H 500"
 ML_DBASE=""
 
-# Poly/ML 5.1 on 64bit Linux
+# Poly/ML 5.1
+#ML_PLATFORM=x86-linux
+#ML_HOME=/usr/local/polyml/x86-linux
+#ML_SYSTEM=polyml-5.1
+#ML_OPTIONS="-H 500"
+
+# Poly/ML 5.1 (64 bit)
 #ML_PLATFORM=x86_64-linux
 #ML_HOME=/usr/local/polyml/x86_64-linux
 #ML_SYSTEM=polyml-5.1
 #ML_OPTIONS="-H 1000"
 
-# Poly/ML 5.1 on Cygwin
-#ML_PLATFORM=x86-cygwin
-#ML_HOME=/usr/local/polyml/x86-cygwin
-#ML_SYSTEM=polyml-5.1
-#ML_OPTIONS="-H 500"
-#POLY_LINK_OPTIONS="-lstdc++"
-
 # Poly/ML 4.2.0
 #ML_PLATFORM=x86-linux
 #ML_HOME=/usr/local/polyml/x86-linux
 #ML_SYSTEM=polyml-4.2.0
 #ML_OPTIONS="-H 80"
 
-# Standard ML of New Jersey 110 or later
-#SMLNJ_CYGWIN_RUNTIME=1
+# Standard ML of New Jersey (slow!)
 #ML_SYSTEM=smlnj-110
-#ML_HOME="$ISABELLE_HOME/contrib/smlnj/bin"
+#ML_HOME="/usr/local/smlnj/bin"
 #ML_OPTIONS="@SMLdebug=/dev/null"
 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
+#SMLNJ_CYGWIN_RUNTIME=1
 
-# Moscow ML 2.00 or later (experimental!)
+# Moscow ML 2.00 (experimental!)
 #ML_SYSTEM=mosml
-#ML_HOME="$ISABELLE_HOME/contrib/mosml/bin"
+#ML_HOME="/usr/local/mosml/bin"
+#ML_OPTIONS=""
+#ML_PLATFORM=""
+
+# Alice 1.4 (experimental!)
+#ML_SYSTEM=alice
+#ML_HOME="/usr/local/alice/bin"
 #ML_OPTIONS=""
 #ML_PLATFORM=""
 
@@ -69,12 +74,6 @@
 #ML_SUFFIX=".psv"
 #ML_PLATFORM=""
 
-# Alice 1.4 (experimental!)
-#ML_SYSTEM=alice
-#ML_HOME="/usr/local/alice/bin"
-#ML_OPTIONS=""
-#ML_PLATFORM=""
-
 
 ###
 ### Compilation options (cf. isatool usedir)