1.1 --- a/etc/settings	Fri Dec 12 22:43:10 1997 +0100
     1.2 +++ b/etc/settings	Sat Dec 13 17:22:15 1997 +0100
     1.3 @@ -27,9 +27,14 @@
     1.4  #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
     1.5  #ML_OPTIONS=""
     1.6  
     1.7 -# Standard ML of New Jersey 1.09.27 or later
     1.8 -#ML_SYSTEM=smlnj-1.09
     1.9 -#ML_HOME=/usr/local/sml109.27/bin
    1.10 +# Standard ML of New Jersey 109.27 to 109.33
    1.11 +#ML_SYSTEM=smlnj-109
    1.12 +#ML_HOME=/usr/proj/smlnj/109.32/bin
    1.13 +#ML_OPTIONS="@SMLdebug=/dev/null"
    1.14 +
    1.15 +# Standard ML of New Jersey 110 or later
    1.16 +#ML_SYSTEM=smlnj-110
    1.17 +#ML_HOME=/usr/proj/smlnj/110/bin
    1.18  #ML_OPTIONS="@SMLdebug=/dev/null"
    1.19  
    1.20