diff -r f8595f6d39a5 -r 66e7a3131fe3 src/Pure/System/command_line.ML --- 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;