1.1 --- a/etc/settings	Mon Jan 14 17:31:45 2002 +0100
     1.2 +++ b/etc/settings	Mon Jan 14 17:43:44 2002 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4    ML_PLATFORM=x86-linux
     1.5    ML_HOME=/usr/bin
     1.6    ML_DBASE=/usr/lib/poly/ML_dbase
     1.7 -  ML_OPTIONS="-h 30000"
     1.8 +  ML_OPTIONS="-h 15000"
     1.9  else
    1.10    #... or rather a self-contained multi-platform installation
    1.11    POLYML_HOME=$(choosefrom \
    1.12 @@ -33,7 +33,7 @@
    1.13    ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
    1.14    ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
    1.15    ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    1.16 -  ML_OPTIONS="-h 30000"
    1.17 +  ML_OPTIONS="-h 15000"
    1.18  fi
    1.19  
    1.20  # Standard ML of New Jersey 110 or later