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