etc/settings
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