maintain PolyML.Compiler.printInAlphabeticalOrder in polyml.ML;
authorwenzelm
Sat, 20 Oct 2007 20:32:23 +0200
changeset 25124 a7dd8d3bf969
parent 25123 8831ca91f43f
child 25125 23d4cab56a7f
maintain PolyML.Compiler.printInAlphabeticalOrder in polyml.ML;
lib/scripts/run-polyml-5.0
--- a/lib/scripts/run-polyml-5.0	Sat Oct 20 20:31:50 2007 +0200
+++ b/lib/scripts/run-polyml-5.0	Sat Oct 20 20:32:23 2007 +0200
@@ -67,7 +67,7 @@
 
 ## run it!
 
-MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $EXIT $COMMIT $MLTEXT"
+MLTEXT="$EXIT $COMMIT $MLTEXT"
 MLEXIT="commit();"
 
 if [ -z "$TERMINATE" ]; then