# HG changeset patch # User wenzelm # Date 1192905186 -7200 # Node ID 23d4cab56a7f116669e656e829ba409e93dc4824 # Parent a7dd8d3bf9692ac5d6ca6f54785d8e61f2fdb348 discontinued support for 4.1.1, 4.1.2; maintain PolyML.Compiler.printInAlphabeticalOrder; diff -r a7dd8d3bf969 -r 23d4cab56a7f src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Sat Oct 20 20:32:23 2007 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Sat Oct 20 20:33:06 2007 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/ML-Systems/polyml.ML ID: $Id$ -Compatibility file for Poly/ML (version 4.1.x and 4.2.0). +Compatibility file for Poly/ML (version 4.1.3, 4.1.4 and 4.2.0). *) use "ML-Systems/exn.ML"; @@ -11,8 +11,11 @@ (** ML system and platform related **) +(* Compiler options *) + val ml_system_fix_ints = false; +PolyML.Compiler.printInAlphabeticalOrder := false; PolyML.Compiler.maxInlineSize := 80;