| changeset 48443 | 6f2762eedca0 |
| parent 48190 | 76b6207eb000 |
| child 48685 | 9f9b289964dc |
--- a/Admin/mira.py Mon Jul 23 09:28:03 2012 +0200 +++ b/Admin/mira.py Mon Jul 23 12:05:48 2012 +0200 @@ -492,8 +492,8 @@ smlnj_settings = ''' ML_SYSTEM=smlnj -ML_HOME="/home/smlnj/110.72/bin" -ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256" +ML_HOME="/home/smlnj/110.74/bin" +ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024" ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") '''