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