| changeset 11485 | f7157bdc1e70 |
| parent 10555 | 2323ec838401 |
| child 12111 | d942348d8faf |
--- 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