tuned ML_OPTIONS for SML/NJ -- for improved performance;
authorwenzelm
Sat, 07 Nov 2009 16:54:13 +0100
changeset 33502cf392b693385
parent 33501 31872dd275c8
child 33508 70026e20fa4c
tuned ML_OPTIONS for SML/NJ -- for improved performance;
Admin/isatest/settings/at-sml-dev-e
etc/settings
     1.1 --- a/Admin/isatest/settings/at-sml-dev-e	Sat Nov 07 08:18:12 2009 +0100
     1.2 +++ b/Admin/isatest/settings/at-sml-dev-e	Sat Nov 07 16:54:13 2009 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4  # Standard ML of New Jersey 110 or later
     1.5  ML_SYSTEM=smlnj
     1.6  ML_HOME="/home/smlnj/110.67/bin"
     1.7 -ML_OPTIONS="@SMLdebug=/dev/null"
     1.8 +ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
     1.9  ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
    1.10  
    1.11  ISABELLE_HOME_USER="$HOME/isabelle-at-sml-dev-e"
     2.1 --- a/etc/settings	Sat Nov 07 08:18:12 2009 +0100
     2.2 +++ b/etc/settings	Sat Nov 07 16:54:13 2009 +0100
     2.3 @@ -51,7 +51,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"
     2.8 +#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
     2.9  #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
    2.10  #SMLNJ_CYGWIN_RUNTIME=1
    2.11