# HG changeset patch
# User wenzelm
# Date 850728530 -3600
# Node ID a0727e4d94534f6ae5d6722b16c5698b769c546c
# Parent  f4505fe0bd22606c6a4ec36593b929ac8e401236
added smlnj-0.93;

diff -r f4505fe0bd22 -r a0727e4d9453 etc/settings
--- 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