Skip to content

Commit fe63582

Browse files
committed
fix: terminate fileworker and watchdog when pipe is closed
1 parent 820587c commit fe63582

File tree

2 files changed

+4
-0
lines changed

2 files changed

+4
-0
lines changed

src/Lean/Server/FileWorker.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1098,5 +1098,7 @@ def workerMain (opts : Options) : IO UInt32 := do
10981098
catch err =>
10991099
e.putStrLn err.toString
11001100
IO.Process.forceExit 1 -- Terminate all tasks of this process
1101+
finally
1102+
IO.Process.forceExit (α := UInt32) 1
11011103

11021104
end Lean.Server.FileWorker

src/Lean/Server/Watchdog.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1809,5 +1809,7 @@ def watchdogMain (args : List String) : IO UInt32 := do
18091809
catch err =>
18101810
e.putStrLn s!"Watchdog error: {err}"
18111811
IO.Process.forceExit 1 -- Terminate all tasks of this process
1812+
finally
1813+
IO.Process.forceExit (α := UInt32) 1
18121814

18131815
end Lean.Server.Watchdog

0 commit comments

Comments
 (0)