diff -r e3f3854f460e -r 01e2bd5b4027 src/Pure/build --- a/src/Pure/build Mon Feb 29 16:25:51 2016 +0100 +++ b/src/Pure/build Mon Feb 29 16:29:52 2016 +0100 @@ -68,7 +68,6 @@ "$ISABELLE_PROCESS" \ -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ -e "structure Isar = struct fun main () = () end;" \ - -e "ml_prompts \"ML> \" \"ML# \";" \ -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \ -q RAW_ML_SYSTEM && chmod -w "$OUTPUT" fi @@ -81,7 +80,6 @@ rm -f "$OUTPUT" "$ISABELLE_PROCESS" \ -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ - -e "ml_prompts \"ML> \" \"ML# \";" \ -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \ -q RAW_ML_SYSTEM && chmod -w "$OUTPUT" fi