diff -r 50425e4c3910 -r 3f02bc5a5a03 src/Pure/System/command_line.ML
--- a/src/Pure/System/command_line.ML	Mon Mar 30 11:59:44 2020 +0200
+++ b/src/Pure/System/command_line.ML	Mon Mar 30 19:39:11 2020 +0200
@@ -6,6 +6,7 @@
 
 signature COMMAND_LINE =
 sig
+  exception EXIT of int
   val tool: (unit -> int) -> unit
   val tool0: (unit -> unit) -> unit
 end;
@@ -13,15 +14,17 @@
 structure Command_Line: COMMAND_LINE =
 struct
 
+exception EXIT of int;
+
 fun tool body =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val rc =
-        restore_attributes body () handle exn =>
-          Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
+        restore_attributes body ()
+          handle EXIT rc => rc
+            | exn => Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
     in exit rc end) ();
 
 fun tool0 body = tool (fn () => (body (); 0));
 
 end;
-