| changeset 3349 | 943d1630f003 |
| parent 3312 | 6ec687d436aa |
| child 3362 | 0b268cff9344 |
--- a/etc/settings Mon May 26 12:54:40 1997 +0200 +++ b/etc/settings Mon May 26 13:45:39 1997 +0200 @@ -32,7 +32,7 @@ #ML_HOME=/usr/local/sml107/bin #ML_OPTIONS="@SMLdebug=/dev/null" -# Standard ML of New Jersey 1.09.27 +# 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"