# 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;