etc/settings
changeset 2410 a0727e4d9453
parent 2352 562cb286138e
child 2426 dc9dcdb43b4f
--- a/etc/settings	Mon Dec 16 10:05:16 1996 +0100
+++ b/etc/settings	Mon Dec 16 10:28:50 1996 +0100
@@ -45,7 +45,7 @@
 
 ## ML compilers and options
 
-#ML_SYSTEM=polyml-2.07
+#ML_SYSTEM=polyml-2.x
 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2
 #ML_OPTIONS="-h 30000"
 
@@ -55,6 +55,8 @@
 LM_LICENSE_FILE=$ML_HOME/license.dat
 
 #ML_SYSTEM=smlnj-0.93
+#ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
+#ML_OPTIONS=""
 
 #ML_SYSTEM=smlnj-1.07
 #ML_HOME=/usr/local/sml107