1.1 --- a/Admin/mira.py Mon Jul 23 09:28:03 2012 +0200
1.2 +++ b/Admin/mira.py Mon Jul 23 12:05:48 2012 +0200
1.3 @@ -492,8 +492,8 @@
1.4
1.5 smlnj_settings = '''
1.6 ML_SYSTEM=smlnj
1.7 -ML_HOME="/home/smlnj/110.72/bin"
1.8 -ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
1.9 +ML_HOME="/home/smlnj/110.74/bin"
1.10 +ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
1.11 ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
1.12 '''
1.13
2.1 --- a/etc/settings Mon Jul 23 09:28:03 2012 +0200
2.2 +++ b/etc/settings Mon Jul 23 12:05:48 2012 +0200
2.3 @@ -45,7 +45,7 @@
2.4 # Standard ML of New Jersey (slow!)
2.5 #ML_SYSTEM=smlnj-110
2.6 #ML_HOME="/usr/local/smlnj/bin"
2.7 -#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
2.8 +#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
2.9 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
2.10 #SMLNJ_CYGWIN_RUNTIME=1
2.11