| changeset 48443 | 6f2762eedca0 |
| parent 48207 | 40fab092d2a2 |
| child 48449 | 2d987dad7c3e |
--- a/etc/settings Mon Jul 23 09:28:03 2012 +0200 +++ b/etc/settings Mon Jul 23 12:05:48 2012 +0200 @@ -45,7 +45,7 @@ # Standard ML of New Jersey (slow!) #ML_SYSTEM=smlnj-110 #ML_HOME="/usr/local/smlnj/bin" -#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256" +#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024" #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") #SMLNJ_CYGWIN_RUNTIME=1