From ebe3317e3c289d569b6cd670a2ed77859579ad32 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 24 Jul 2024 16:28:16 +0200 Subject: [PATCH] doc: typo Co-authored-by: Sebastian Ullrich --- src/Lean/Server/Watchdog.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 539b17ce7644..95c8a6e50e8b 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -961,7 +961,7 @@ section MainLoop for (_, fw) in workers do -- When the forwarding task crashes, its return value will be stuck at -- `WorkerEvent.crashed _`. - -- We do not want to handle this event only once, not over and over again, + -- We want to handle this event only once, not over and over again, -- so once the state becomes `WorkerState.crashed _ .fileWorkerToClientForwarding` -- as a result of `WorkerEvent.crashed _`, we stop handling this event until -- eventually the file worker is restarted by a notification from the client.