author | wenzelm |
Thu, 04 Jun 2009 23:42:11 +0200 | |
changeset 31444 | 4fa98c1df7ba |
parent 31443 | c23663825e23 |
child 31450 | d0ffa8fad5bb |
child 31451 | 960688121738 |
child 31461 | d54b743b52a3 |
etc/settings | file | annotate | diff | comparison | revisions |
--- a/etc/settings Thu Jun 04 22:52:53 2009 +0200 +++ b/etc/settings Thu Jun 04 23:42:11 2009 +0200 @@ -41,6 +41,13 @@ #ML_SYSTEM=polyml-5.2.1 #ML_OPTIONS="-H 1000" +# Poly/ML 5.3 (experimental) +#ML_PLATFORM=x86-linux +#ML_HOME=/usr/local/polyml/x86-linux +#ML_SYSTEM=polyml-experimental +#ML_OPTIONS="-H 500" +#ML_SOURCES="$ML_HOME/../src" + # Standard ML of New Jersey (slow!) #ML_SYSTEM=smlnj-110 #ML_HOME="/usr/local/smlnj/bin"