1.1 --- a/etc/settings	Mon Nov 09 20:47:39 2009 +0100
     1.2 +++ b/etc/settings	Mon Nov 09 21:30:54 2009 +0100
     1.3 @@ -29,23 +29,18 @@
     1.4  ML_OPTIONS="-H 200"
     1.5  ML_SOURCES="$ML_HOME/../src"
     1.6  
     1.7 -# Poly/ML 5.2.1
     1.8 +# Poly/ML 5.3.0
     1.9  #ML_PLATFORM=x86-linux
    1.10  #ML_HOME=/usr/local/polyml/x86-linux
    1.11 -#ML_SYSTEM=polyml-5.2.1
    1.12 +#ML_SYSTEM=polyml-5.3.0
    1.13  #ML_OPTIONS="-H 500"
    1.14 +#ML_SOURCES="$ML_HOME/../src"
    1.15  
    1.16 -# Poly/ML 5.2.1 (64 bit)
    1.17 +# Poly/ML 5.3.0 (64 bit)
    1.18  #ML_PLATFORM=x86_64-linux
    1.19  #ML_HOME=/usr/local/polyml/x86_64-linux
    1.20 -#ML_SYSTEM=polyml-5.2.1
    1.21 +#ML_SYSTEM=polyml-5.3.0
    1.22  #ML_OPTIONS="-H 1000"
    1.23 -
    1.24 -# Poly/ML 5.3 (experimental)
    1.25 -#ML_PLATFORM=x86-linux
    1.26 -#ML_HOME=/usr/local/polyml/x86-linux
    1.27 -#ML_SYSTEM=polyml-experimental
    1.28 -#ML_OPTIONS="-H 500"
    1.29  #ML_SOURCES="$ML_HOME/../src"
    1.30  
    1.31  # Standard ML of New Jersey (slow!)