--- a/etc/settings Wed Jul 05 18:27:55 2000 +0200
+++ b/etc/settings Thu Jul 06 00:08:24 2000 +0200
@@ -27,16 +27,16 @@
#ML_OPTIONS="@SMLdebug=/dev/null"
#ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX)
-# MLWorks 2.0 or later
-#ML_SYSTEM=mlworks
-#ML_HOME=/usr/local/mlworks/bin
-#ML_OPTIONS=""
+# Moscow ML 2.00 or later (experimental!)
+#ML_SYSTEM=mosml
+#ML_HOME=$ISABELLE_HOME/../mosml/bin
#ML_PLATFORM=""
+#ML_OPTIONS=""
-# Poly/ML 2.x
-#ML_SYSTEM=polyml-2.07
-#ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2
-#ML_OPTIONS="-h 30000"
+# MLWorks 2.0
+#ML_SYSTEM=mlworks
+#ML_HOME=$ISABELLE_HOME/../mlworks/bin
+#ML_OPTIONS=""
#ML_PLATFORM=""
# Standard ML of New Jersey 0.93