changeset 8361 | ac19e5abbfb1 |
parent 7277 | bb9502f9154a |
child 9789 | 7e5e6c47c0b5 |
--- a/src/Pure/mk Wed Mar 08 17:40:24 2000 +0100 +++ b/src/Pure/mk Wed Mar 08 17:41:40 2000 +0100 @@ -86,7 +86,7 @@ $ISABELLE \ -e "val ml_system = \"$ML_SYSTEM\";" \ -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ - -q -w RAW_ML_SYSTEM Pure > $LOG 2>&1 + -c -q -w RAW_ML_SYSTEM Pure > $LOG 2>&1 RC=$? else ITEM="RAW"