author | wenzelm |
Mon, 01 Aug 2005 19:20:22 +0200 | |
changeset 16969 | e26915e01d15 |
parent 16968 | 5cb40c8b1f10 |
child 16970 | c1ef99e08c39 |
--- 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