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