# HG changeset patch
# User wenzelm
# Date 1123010946 -7200
# Node ID 69c415d4488335ebb60575fa36ce4e947b6e37b4
# Parent  6a0d8ecf65f10dd6fc531abc4824e29cf0155426
tuned ML_OPTIONS;

diff -r 6a0d8ecf65f1 -r 69c415d44883 etc/settings
--- a/etc/settings	Tue Aug 02 19:47:14 2005 +0200
+++ b/etc/settings	Tue Aug 02 21:29:06 2005 +0200
@@ -27,7 +27,7 @@
   "/opt/polyml/$ML_PLATFORM" \
   $POLY_HOME)
 ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
-ML_OPTIONS="-h 50000"
+ML_OPTIONS="-H 80"
 
 # Standard ML of New Jersey 110 or later
 #SMLNJ_CYGWIN_RUNTIME=1