1.1 --- a/etc/settings	Mon Dec 16 10:05:16 1996 +0100
     1.2 +++ b/etc/settings	Mon Dec 16 10:28:50 1996 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4  
     1.5  ## ML compilers and options
     1.6  
     1.7 -#ML_SYSTEM=polyml-2.07
     1.8 +#ML_SYSTEM=polyml-2.x
     1.9  #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2
    1.10  #ML_OPTIONS="-h 30000"
    1.11  
    1.12 @@ -55,6 +55,8 @@
    1.13  LM_LICENSE_FILE=$ML_HOME/license.dat
    1.14  
    1.15  #ML_SYSTEM=smlnj-0.93
    1.16 +#ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
    1.17 +#ML_OPTIONS=""
    1.18  
    1.19  #ML_SYSTEM=smlnj-1.07
    1.20  #ML_HOME=/usr/local/sml107