diff -r fb25f00d1c70 -r c44c83006891 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"