1.1 --- a/etc/settings	Mon May 26 12:54:40 1997 +0200
     1.2 +++ b/etc/settings	Mon May 26 13:45:39 1997 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  #ML_HOME=/usr/local/sml107/bin
     1.5  #ML_OPTIONS="@SMLdebug=/dev/null"
     1.6  
     1.7 -# Standard ML of New Jersey 1.09.27
     1.8 +# Standard ML of New Jersey 1.09.27, or later
     1.9  #ML_SYSTEM=smlnj-1.09
    1.10  #ML_HOME=/usr/local/sml109.27/bin
    1.11  #ML_OPTIONS="@SMLdebug=/dev/null"