--- a/src/Pure/System/command_line.ML Thu Apr 02 12:19:09 2020 +0200
+++ b/src/Pure/System/command_line.ML Thu Apr 02 12:49:53 2020 +0200
@@ -6,22 +6,18 @@
signature COMMAND_LINE =
sig
- exception EXIT of int
val tool: (unit -> unit) -> unit
end;
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 (); 0)
- handle EXIT rc => rc
- | exn => Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
+ handle exn => Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
in exit rc end) ();
end;