author | wenzelm |
Wed, 08 Aug 2001 15:16:38 +0200 | |
changeset 11485 | f7157bdc1e70 |
parent 11484 | 44053d894713 |
child 11486 | 8f32860eac3a |
--- 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