# HG changeset patch
# User wenzelm
# Date 997276598 -7200
# Node ID f7157bdc1e7015a9108b55046427daf839a731dd
# Parent  44053d894713165851f38e9bac6c68ceeed14257
[ "$ML_SYSTEM" = polyml-4.1.1 ] && DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120";

diff -r 44053d894713 -r f7157bdc1e70 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Wed Aug 08 14:57:22 2001 +0200
+++ b/lib/scripts/run-polyml	Wed Aug 08 15:16:38 2001 +0200
@@ -73,6 +73,7 @@
   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"
 else
   COPYDB=true
 fi