etc/settings
changeset 48443 6f2762eedca0
parent 48207 40fab092d2a2
child 48449 2d987dad7c3e
     1.1 --- a/etc/settings	Mon Jul 23 09:28:03 2012 +0200
     1.2 +++ b/etc/settings	Mon Jul 23 12:05:48 2012 +0200
     1.3 @@ -45,7 +45,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 @SMLalloc=256"
     1.8 +#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
     1.9  #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
    1.10  #SMLNJ_CYGWIN_RUNTIME=1
    1.11