| changeset 53658 | 9e8714b4661a |
| parent 50600 | 48c0c3bc40dd |
| child 57172 | bcc6dc6c1d1c |
--- a/Admin/mira.py Mon Sep 16 12:37:54 2013 +0200 +++ b/Admin/mira.py Mon Sep 16 12:51:33 2013 +0200 @@ -324,7 +324,7 @@ smlnj_settings = ''' ML_SYSTEM=smlnj -ML_HOME="/home/smlnj/110.74/bin" +ML_HOME="/home/smlnj/110.76/bin" ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024" ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") '''