author | wenzelm |
Wed, 11 Oct 2006 22:56:10 +0200 | |
changeset 20987 | d1674119d0f9 |
parent 20986 | 808ae04981be |
child 20988 | 0887d0dd3210 |
etc/settings | file | annotate | diff | comparison | revisions |
--- a/etc/settings Wed Oct 11 22:55:23 2006 +0200 +++ b/etc/settings Wed Oct 11 22:56:10 2006 +0200 @@ -40,7 +40,7 @@ #ML_PLATFORM=x86_64-linux #ML_HOME=/usr/local/polyml/x86_64-linux #ML_SYSTEM=polyml-4.9.1 -#ML_OPTIONS="-H 160" +#ML_OPTIONS="-H 500" # Standard ML of New Jersey 110 or later #SMLNJ_CYGWIN_RUNTIME=1