PolyML.Compiler.printInAlphabeticalOrder := false;
authorwenzelm
Mon, 01 Aug 2005 19:20:22 +0200
changeset 16969 e26915e01d15
parent 16968 5cb40c8b1f10
child 16970 c1ef99e08c39
PolyML.Compiler.printInAlphabeticalOrder := false;
lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Mon Aug 01 19:20:21 2005 +0200
+++ b/lib/scripts/run-polyml	Mon Aug 01 19:20:22 2005 +0200
@@ -100,6 +100,14 @@
 
 ## run it!
 
+case "$ML_SYSTEM" in
+  polyml-4.1.[12])
+    ;;
+  polyml-4.1.*)
+    MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $MLTEXT"
+    ;;
+esac
+
 if [ -z "$TERMINATE" ]; then
   FEEDER_OPTS=""
 else