# HG changeset patch # User wenzelm # Date 1379328693 -7200 # Node ID 9e8714b4661a7c6f553e12958ac9332a2ee3bdf7 # Parent 64942a1f718772e5cefe20f410bc374b7f3f8fed updated to smlnj 110.76; diff -r 64942a1f7187 -r 9e8714b4661a Admin/isatest/settings/at-sml-dev-e --- a/Admin/isatest/settings/at-sml-dev-e Mon Sep 16 12:37:54 2013 +0200 +++ b/Admin/isatest/settings/at-sml-dev-e Mon Sep 16 12:51:33 2013 +0200 @@ -3,7 +3,7 @@ init_components /home/isabelle/contrib "$HOME/admin/components/main" ML_SYSTEM=smlnj -ML_HOME="/home/smlnj/110.75/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") diff -r 64942a1f7187 -r 9e8714b4661a Admin/mira.py --- 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") '''