ML_OPTIONS="-h 15000" (used to be 30000);
authorwenzelm
Mon, 14 Jan 2002 17:43:44 +0100
changeset 12752 f80407a8deda
parent 12751 66ed22799ce8
child 12753 3a62df7ae926
ML_OPTIONS="-h 15000" (used to be 30000);
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