polyml: default heap size is back to -H 200 (people are still using
authorwenzelm
Wed, 28 Nov 2007 19:54:50 +0100
changeset 255007a284dc85326
parent 25499 7e0ad4838ce9
child 25501 845883bd3a6b
polyml: default heap size is back to -H 200 (people are still using
machines with < 1GB of memory; no need to workaround heap problems of
polyml-5.0 anymore);
etc/settings
     1.1 --- a/etc/settings	Wed Nov 28 18:39:53 2007 +0100
     1.2 +++ b/etc/settings	Wed Nov 28 19:54:50 2007 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4    "/opt/polyml/$ML_PLATFORM" \
     1.5    $POLY_HOME)
     1.6  ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
     1.7 -ML_OPTIONS="-H 500"
     1.8 +ML_OPTIONS="-H 200"
     1.9  ML_DBASE=""
    1.10  
    1.11  # Poly/ML 5.1