changeset 78672 | fcdfd3251892 |
parent 75620 | 44815dc2b8f9 |
child 78681 | 38fe769658be |
--- a/src/Pure/System/isabelle_system.ML Tue Sep 19 13:02:48 2023 +0200 +++ b/src/Pure/System/isabelle_system.ML Tue Sep 19 13:12:13 2023 +0200 @@ -68,7 +68,7 @@ if head = Bash.server_uuid andalso length args = 1 then loop (SOME (hd args)) s else if head = Bash.server_interrupt andalso null args then - raise Exn.Interrupt + Exn.interrupt () else if head = Bash.server_failure andalso length args = 1 then raise Fail (hd args) else if head = Bash.server_result andalso length args >= 4 then