option -S 180;
authorwenzelm
Fri, 01 Mar 2002 22:32:10 +0100
changeset 13002 e844d0ee15d5
parent 13001 40ba2eee948e
child 13003 3d5807d45439
option -S 180;
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