| changeset 20987 | d1674119d0f9 |
| parent 20764 | 4aa5c89b933e |
| child 21171 | 7b4fb2a2c75e |
--- 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