removed smlnj-1.07;
authorwenzelm
Tue, 05 Aug 1997 17:21:24 +0200
changeset 3596 c44c83006891
parent 3595 fb25f00d1c70
child 3597 3ac6d6bcae42
removed smlnj-1.07;
etc/settings
--- a/etc/settings	Tue Aug 05 17:03:11 1997 +0200
+++ b/etc/settings	Tue Aug 05 17:21:24 1997 +0200
@@ -27,12 +27,7 @@
 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
 #ML_OPTIONS=""
 
-# Standard ML of New Jersey 1.07
-#ML_SYSTEM=smlnj-1.07
-#ML_HOME=/usr/local/sml107/bin
-#ML_OPTIONS="@SMLdebug=/dev/null"
-
-# Standard ML of New Jersey 1.09.27, 1.09.28, or later
+# Standard ML of New Jersey 1.09.27 or later
 #ML_SYSTEM=smlnj-1.09
 #ML_HOME=/usr/local/sml109.27/bin
 #ML_OPTIONS="@SMLdebug=/dev/null"