option -S 180;
authorwenzelm
Fri Mar 01 22:32:10 2002 +0100 (2002-03-01)
changeset 13002e844d0ee15d5
parent 13001 40ba2eee948e
child 13003 3d5807d45439
option -S 180;
lib/scripts/run-polyml
     1.1 --- a/lib/scripts/run-polyml	Fri Mar 01 22:31:48 2002 +0100
     1.2 +++ b/lib/scripts/run-polyml	Fri Mar 01 22:32:10 2002 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4    INFILE="$ML_DBASE"
     1.5    MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
     1.6    [ "$ML_SYSTEM" = polyml-4.1.1 -o "$ML_SYSTEM" = polyml-4.1.2 ] && \
     1.7 -    DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120"
     1.8 +    DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180"
     1.9  else
    1.10    COPYDB=true
    1.11  fi