changeset 25023 | 52eb78ebb370 |
parent 24851 | 4e304aac841a |
child 25125 | 23d4cab56a7f |
--- a/src/Pure/ML-Systems/polyml.ML Sat Oct 13 17:16:45 2007 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Sat Oct 13 17:16:46 2007 +0200 @@ -8,10 +8,13 @@ use "ML-Systems/multithreading.ML"; use "ML-Systems/time_limit.ML"; + +(** ML system and platform related **) + val ml_system_fix_ints = false; +PolyML.Compiler.maxInlineSize := 80; -(** ML system and platform related **) (* String compatibility *)