--- a/src/Pure/System/command_line.ML Mon Feb 29 16:12:47 2016 +0100
+++ b/src/Pure/System/command_line.ML Mon Feb 29 16:24:20 2016 +0100
@@ -19,7 +19,7 @@
val rc =
restore_attributes body () handle exn =>
Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
- in if rc = 0 then () else exit rc end) ();
+ in exit rc end) ();
fun tool0 body = tool (fn () => (body (); 0));
--- a/src/Pure/build Mon Feb 29 16:12:47 2016 +0100
+++ b/src/Pure/build Mon Feb 29 16:24:20 2016 +0100
@@ -82,10 +82,7 @@
"$ISABELLE_PROCESS" \
-e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
-e "ml_prompts \"ML> \" \"ML# \";" \
- -e "Command_Line.tool0 Session.finish;" \
- -e "Options.reset_default ();" \
- -e "Session.shutdown ();" \
- -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \
+ -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
fi