author | wenzelm |
Tue, 05 Aug 1997 17:21:24 +0200 | |
changeset 3596 | c44c83006891 |
parent 3595 | fb25f00d1c70 |
child 3597 | 3ac6d6bcae42 |
etc/settings | file | annotate | diff | comparison | revisions |
--- 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"