--- a/etc/settings Sun May 31 14:15:07 2009 +0200
+++ b/etc/settings Sun May 31 14:16:32 2009 +0200
@@ -29,16 +29,16 @@
ML_OPTIONS="-H 200"
ML_DBASE=""
-# Poly/ML 5.1
+# Poly/ML 5.2.1
#ML_PLATFORM=x86-linux
#ML_HOME=/usr/local/polyml/x86-linux
-#ML_SYSTEM=polyml-5.1
+#ML_SYSTEM=polyml-5.2.1
#ML_OPTIONS="-H 500"
-# Poly/ML 5.1 (64 bit)
+# Poly/ML 5.2.1 (64 bit)
#ML_PLATFORM=x86_64-linux
#ML_HOME=/usr/local/polyml/x86_64-linux
-#ML_SYSTEM=polyml-5.1
+#ML_SYSTEM=polyml-5.2.1
#ML_OPTIONS="-H 1000"
# Standard ML of New Jersey (slow!)