changeset 33502 | cf392b693385 |
parent 32426 | dd25b3055c4e |
child 33540 | edf497b5b5d2 |
1.1 --- a/etc/settings Sat Nov 07 08:18:12 2009 +0100 1.2 +++ b/etc/settings Sat Nov 07 16:54:13 2009 +0100 1.3 @@ -51,7 +51,7 @@ 1.4 # Standard ML of New Jersey (slow!) 1.5 #ML_SYSTEM=smlnj-110 1.6 #ML_HOME="/usr/local/smlnj/bin" 1.7 -#ML_OPTIONS="@SMLdebug=/dev/null" 1.8 +#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256" 1.9 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") 1.10 #SMLNJ_CYGWIN_RUNTIME=1 1.11