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