# HG changeset patch
# User wenzelm
# Date 1011298031 -3600
# Node ID 76f3dd2f151af7fa0d02380f800d68bd0bf4b17d
# Parent  787ecc2ac737ad09f7950e4048f967808e75d43c
cover polyml-4.1.2;

diff -r 787ecc2ac737 -r 76f3dd2f151a lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Thu Jan 17 21:07:00 2002 +0100
+++ b/lib/scripts/run-polyml	Thu Jan 17 21:07:11 2002 +0100
@@ -73,7 +73,8 @@
   check_file "$ML_DBASE_PREFIX$ML_DBASE"
   INFILE="$ML_DBASE"
   MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
-  [ "$ML_SYSTEM" = polyml-4.1.1 ] && DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120"
+  [ "$ML_SYSTEM" = polyml-4.1.1 -o "$ML_SYSTEM" = polyml-4.1.2 ] && \
+    DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120"
 else
   COPYDB=true
 fi