| changeset 21653 | 219924615db6 |
| parent 21489 | 4ce7425c8372 |
| child 21812 | 2776dcfd5617 |
--- a/etc/settings Tue Dec 05 18:32:54 2006 +0100 +++ b/etc/settings Tue Dec 05 18:33:29 2006 +0100 @@ -36,10 +36,10 @@ #ML_SYSTEM=polyml-4.2.0 #ML_OPTIONS="-H 80" -# Poly/ML 4.9.1 (experimental!) +# Poly/ML 5.0 #ML_PLATFORM=x86_64-linux #ML_HOME=/usr/local/polyml/x86_64-linux -#ML_SYSTEM=polyml-4.9.1 +#ML_SYSTEM=polyml-5.0 #ML_OPTIONS="-H 500" # Standard ML of New Jersey 110 or later