# HG changeset patch # User wenzelm # Date 1128807795 -7200 # Node ID 81c113e4d6fc229d13bc30c9d9111c944155fbea # Parent cc5dbc24e56137dc03569e8612032ff3e82f5704 tuned Memory.hilim; diff -r cc5dbc24e561 -r 81c113e4d6fc src/Pure/ML-Systems/poplogml.ML --- a/src/Pure/ML-Systems/poplogml.ML Sat Oct 08 23:43:14 2005 +0200 +++ b/src/Pure/ML-Systems/poplogml.ML Sat Oct 08 23:43:15 2005 +0200 @@ -8,7 +8,7 @@ (* Compiler and runtime options *) val _ = Compile.filetype := ".ML"; -val _ = Memory.hilim := 10 * ! Memory.hilim; +val _ = Memory.hilim := let fun MB n = n div 4 * 1024 * 1024 in MB 120 end; val _ = Memory.stacklim := 10 * ! Memory.stacklim; fun pointer_eq (_: 'a, _: 'a) = false;