| changeset 78720 | 909dc00766a0 |
| parent 78716 | 97dfba4405e3 |
| child 78725 | 3c02ad5a1586 |
--- a/src/Pure/System/command_line.ML Tue Sep 26 14:29:55 2023 +0200 +++ b/src/Pure/System/command_line.ML Tue Sep 26 14:42:33 2023 +0200 @@ -13,11 +13,11 @@ struct fun tool body = - Thread_Attributes.uninterruptible (fn run => fn () => + Thread_Attributes.uninterruptible_body (fn run => let val rc = (run body (); 0) handle exn => ((Runtime.exn_error_message exn; Exn.failure_rc exn) handle err => Exn.failure_rc err); - in exit rc end) (); + in exit rc end); end;