clarified exit code for the rare situation where Runtime.exn_error_message might fail;
authorwenzelm
Tue, 22 Apr 2014 12:05:02 +0200
changeset 56630 d06c44532706
parent 56629 ca302c495bca
child 56631 89269bb8e7ca
clarified exit code for the rare situation where Runtime.exn_error_message might fail;
src/Pure/System/command_line.ML
--- 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));