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