# HG changeset patch
# User wenzelm
# Date 1015018330 -3600
# Node ID e844d0ee15d51ed0cd89fcff924cd844df52e227
# Parent  40ba2eee948ed12c14f449bfbacab1626880186a
option -S 180;

diff -r 40ba2eee948e -r e844d0ee15d5 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Fri Mar 01 22:31:48 2002 +0100
+++ b/lib/scripts/run-polyml	Fri Mar 01 22:32:10 2002 +0100
@@ -74,7 +74,7 @@
   INFILE="$ML_DBASE"
   MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
   [ "$ML_SYSTEM" = polyml-4.1.1 -o "$ML_SYSTEM" = polyml-4.1.2 ] && \
-    DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120"
+    DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180"
 else
   COPYDB=true
 fi