1.1 --- a/etc/settings	Thu Jun 04 22:52:53 2009 +0200
     1.2 +++ b/etc/settings	Thu Jun 04 23:42:11 2009 +0200
     1.3 @@ -41,6 +41,13 @@
     1.4  #ML_SYSTEM=polyml-5.2.1
     1.5  #ML_OPTIONS="-H 1000"
     1.6  
     1.7 +# Poly/ML 5.3 (experimental)
     1.8 +#ML_PLATFORM=x86-linux
     1.9 +#ML_HOME=/usr/local/polyml/x86-linux
    1.10 +#ML_SYSTEM=polyml-experimental
    1.11 +#ML_OPTIONS="-H 500"
    1.12 +#ML_SOURCES="$ML_HOME/../src"
    1.13 +
    1.14  # Standard ML of New Jersey (slow!)
    1.15  #ML_SYSTEM=smlnj-110
    1.16  #ML_HOME="/usr/local/smlnj/bin"