# HG changeset patch
# User wenzelm
# Date 1131977699 -3600
# Node ID b7c3136f604dc9268172e99689e931f7bf7060a9
# Parent  cbed396ecb1c583b67725da91d3dbc5009d81af6
support for polyml-4.2.0;

diff -r cbed396ecb1c -r b7c3136f604d lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Mon Nov 14 15:14:32 2005 +0100
+++ b/lib/scripts/run-polyml	Mon Nov 14 15:14:59 2005 +0100
@@ -77,7 +77,7 @@
     polyml-4.1.[12])
       DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180"
       ;;
-    polyml-4.1.*)
+    polyml-4.1.[34] | polyml-4.2.*)
       DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
       ;;
   esac
@@ -108,7 +108,7 @@
 case "$ML_SYSTEM" in
   polyml-4.1.[12])
     ;;
-  polyml-4.1.*)
+  polyml-4.1.[34] | polyml-4.2.*)
     MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $MLTEXT"
     ;;
 esac