--- a/etc/settings Mon Nov 09 20:47:39 2009 +0100
+++ b/etc/settings Mon Nov 09 21:30:54 2009 +0100
@@ -29,23 +29,18 @@
ML_OPTIONS="-H 200"
ML_SOURCES="$ML_HOME/../src"
-# Poly/ML 5.2.1
+# Poly/ML 5.3.0
#ML_PLATFORM=x86-linux
#ML_HOME=/usr/local/polyml/x86-linux
-#ML_SYSTEM=polyml-5.2.1
+#ML_SYSTEM=polyml-5.3.0
#ML_OPTIONS="-H 500"
+#ML_SOURCES="$ML_HOME/../src"
-# Poly/ML 5.2.1 (64 bit)
+# Poly/ML 5.3.0 (64 bit)
#ML_PLATFORM=x86_64-linux
#ML_HOME=/usr/local/polyml/x86_64-linux
-#ML_SYSTEM=polyml-5.2.1
+#ML_SYSTEM=polyml-5.3.0
#ML_OPTIONS="-H 1000"
-
-# Poly/ML 5.3 (experimental)
-#ML_PLATFORM=x86-linux
-#ML_HOME=/usr/local/polyml/x86-linux
-#ML_SYSTEM=polyml-experimental
-#ML_OPTIONS="-H 500"
#ML_SOURCES="$ML_HOME/../src"
# Standard ML of New Jersey (slow!)