# HG changeset patch # User wenzelm # Date 1196276090 -3600 # Node ID 7a284dc853268e355e9b80c5786f3b1fdf9e9c46 # Parent 7e0ad4838ce97fe13838f4db06e9bedddf22fbdb 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); diff -r 7e0ad4838ce9 -r 7a284dc85326 etc/settings --- a/etc/settings Wed Nov 28 18:39:53 2007 +0100 +++ b/etc/settings Wed Nov 28 19:54:50 2007 +0100 @@ -27,7 +27,7 @@ "/opt/polyml/$ML_PLATFORM" \ $POLY_HOME) ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") -ML_OPTIONS="-H 500" +ML_OPTIONS="-H 200" ML_DBASE="" # Poly/ML 5.1