# HG changeset patch
# User wenzelm
# Date 1398161102 -7200
# Node ID d06c44532706e60147fc25df6d71900ed7e5e4ea
# Parent  ca302c495bca3150a20a73acaf580cfbad5e6dd9
clarified exit code for the rare situation where Runtime.exn_error_message might fail;

diff -r ca302c495bca -r d06c44532706 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));