clarified exit code for the rare situation where Runtime.exn_error_message might fail;
--- a/src/Pure/System/command_line.ML Tue Apr 22 12:03:58 2014 +0200
+++ b/src/Pure/System/command_line.ML Tue Apr 22 12:05:02 2014 +0200
@@ -18,7 +18,7 @@
let
val rc =
restore_attributes body () handle exn =>
- Exn.capture_exit 1 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
+ Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
in if rc = 0 then () else exit rc end) ();
fun tool0 body = tool (fn () => (body (); 0));