| changeset 12810 | 76f3dd2f151a |
| parent 12111 | d942348d8faf |
| child 13002 | e844d0ee15d5 |
--- a/lib/scripts/run-polyml Thu Jan 17 21:07:00 2002 +0100 +++ b/lib/scripts/run-polyml Thu Jan 17 21:07:11 2002 +0100 @@ -73,7 +73,8 @@ 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" + [ "$ML_SYSTEM" = polyml-4.1.1 -o "$ML_SYSTEM" = polyml-4.1.2 ] && \ + DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120" else COPYDB=true fi