src/Pure/System/command_line.ML
changeset 78716 97dfba4405e3
parent 78673 90b12b919b5f
child 78720 909dc00766a0
--- a/src/Pure/System/command_line.ML	Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/System/command_line.ML	Tue Sep 26 12:46:31 2023 +0200
@@ -13,10 +13,10 @@
 struct
 
 fun tool body =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible (fn run => fn () =>
     let
       val rc =
-        (restore_attributes body (); 0) handle exn =>
+        (run body (); 0) handle exn =>
           ((Runtime.exn_error_message exn; Exn.failure_rc exn) handle err => Exn.failure_rc err);
     in exit rc end) ();