diff -r 6efff142bb54 -r 6f2762eedca0 etc/settings
--- 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