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