# HG changeset patch
# User wenzelm
# Date 1011026624 -3600
# Node ID f80407a8deda328d72cea04efb7000174edb10af
# Parent  66ed22799ce81e2b2f007c8290d23d7fec9dbed3
ML_OPTIONS="-h 15000" (used to be 30000);

diff -r 66ed22799ce8 -r f80407a8deda etc/settings
--- a/etc/settings	Mon Jan 14 17:31:45 2002 +0100
+++ b/etc/settings	Mon Jan 14 17:43:44 2002 +0100
@@ -21,7 +21,7 @@
   ML_PLATFORM=x86-linux
   ML_HOME=/usr/bin
   ML_DBASE=/usr/lib/poly/ML_dbase
-  ML_OPTIONS="-h 30000"
+  ML_OPTIONS="-h 15000"
 else
   #... or rather a self-contained multi-platform installation
   POLYML_HOME=$(choosefrom \
@@ -33,7 +33,7 @@
   ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
   ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="-h 30000"
+  ML_OPTIONS="-h 15000"
 fi
 
 # Standard ML of New Jersey 110 or later