src/Pure/System/command_line.ML
changeset 78671 66e7a3131fe3
parent 71656 3e121f999120
child 78673 90b12b919b5f
--- a/src/Pure/System/command_line.ML	Sun Sep 17 18:56:35 2023 +0100
+++ b/src/Pure/System/command_line.ML	Tue Sep 19 13:02:48 2023 +0200
@@ -15,9 +15,11 @@
 fun tool body =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
+      fun return_code exn =
+        if Exn.is_interrupt exn then 130 else 2;
       val rc =
-        (restore_attributes body (); 0)
-          handle exn => Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
+        (restore_attributes body (); 0) handle exn =>
+          ((Runtime.exn_error_message exn; return_code exn) handle err => return_code err);
     in exit rc end) ();
 
 end;