# HG changeset patch
# User wenzelm
# Date 882030135 -3600
# Node ID 9bb6502db2ff1a6904cc5fe2f0a93a9851771948
# Parent  b893b3ae8ef3369376268c40d68049be13df283d
smlnj-110;

diff -r b893b3ae8ef3 -r 9bb6502db2ff etc/settings
--- a/etc/settings	Fri Dec 12 22:43:10 1997 +0100
+++ b/etc/settings	Sat Dec 13 17:22:15 1997 +0100
@@ -27,9 +27,14 @@
 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
 #ML_OPTIONS=""
 
-# Standard ML of New Jersey 1.09.27 or later
-#ML_SYSTEM=smlnj-1.09
-#ML_HOME=/usr/local/sml109.27/bin
+# Standard ML of New Jersey 109.27 to 109.33
+#ML_SYSTEM=smlnj-109
+#ML_HOME=/usr/proj/smlnj/109.32/bin
+#ML_OPTIONS="@SMLdebug=/dev/null"
+
+# Standard ML of New Jersey 110 or later
+#ML_SYSTEM=smlnj-110
+#ML_HOME=/usr/proj/smlnj/110/bin
 #ML_OPTIONS="@SMLdebug=/dev/null"