1.1 --- a/etc/settings Sun May 31 14:15:07 2009 +0200
1.2 +++ b/etc/settings Sun May 31 14:16:32 2009 +0200
1.3 @@ -29,16 +29,16 @@
1.4 ML_OPTIONS="-H 200"
1.5 ML_DBASE=""
1.6
1.7 -# Poly/ML 5.1
1.8 +# Poly/ML 5.2.1
1.9 #ML_PLATFORM=x86-linux
1.10 #ML_HOME=/usr/local/polyml/x86-linux
1.11 -#ML_SYSTEM=polyml-5.1
1.12 +#ML_SYSTEM=polyml-5.2.1
1.13 #ML_OPTIONS="-H 500"
1.14
1.15 -# Poly/ML 5.1 (64 bit)
1.16 +# Poly/ML 5.2.1 (64 bit)
1.17 #ML_PLATFORM=x86_64-linux
1.18 #ML_HOME=/usr/local/polyml/x86_64-linux
1.19 -#ML_SYSTEM=polyml-5.1
1.20 +#ML_SYSTEM=polyml-5.2.1
1.21 #ML_OPTIONS="-H 1000"
1.22
1.23 # Standard ML of New Jersey (slow!)