| changeset 3596 | c44c83006891 |
| parent 3364 | 8f225296fade |
| child 3637 | 02ba2acc69c3 |
--- 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"