diff -r fb5e3fcfc10c -r b272d7998193 etc/settings --- a/etc/settings Wed Aug 29 20:18:23 2007 +0200 +++ b/etc/settings Wed Aug 29 22:47:01 2007 +0200 @@ -30,11 +30,18 @@ ML_OPTIONS="-H 500" ML_DBASE="" -# Poly/ML 5.0 +# Poly/ML 5.1 on 64bit Linux #ML_PLATFORM=x86_64-linux #ML_HOME=/usr/local/polyml/x86_64-linux -#ML_SYSTEM=polyml-5.0 +#ML_SYSTEM=polyml-5.1 +#ML_OPTIONS="-H 1000" + +# Poly/ML 5.1 on Cygwin +#ML_PLATFORM=x86-cygwin +#ML_HOME=/usr/local/polyml/x86-cygwin +#ML_SYSTEM=polyml-5.1 #ML_OPTIONS="-H 500" +#POLYML_LINK_OPTIONS="-lstdc++" # Poly/ML 4.2.0 #ML_PLATFORM=x86-linux