changeset 31317 | 1f5740424c69 |
parent 30611 | 591fefcf184e |
child 34282 | 549969a7f582 |
--- a/src/Pure/mk Sun May 31 15:29:43 2009 +0200 +++ b/src/Pure/mk Sun May 31 15:49:35 2009 +0200 @@ -114,7 +114,7 @@ -e "val ml_platform = \"$ML_PLATFORM\";" \ -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ -e "ml_prompts \"ML> \" \"ML# \";" \ - -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 + -f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 RC="$?" fi