From 3651ebb37710103b4f37eb6aad82d22bb992c3ea Mon Sep 17 00:00:00 2001 From: Joscha Date: Wed, 19 Jan 2022 16:07:41 +0100 Subject: [PATCH] fix: don't send worker notification to client --- src/Lean/Server/Watchdog.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 770e607272..dde420569c 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -229,8 +229,9 @@ section ServerM if let some params := params then if let Except.ok params := FromJson.fromJson? $ ToJson.toJson params then handleIleanInfo fw params - -- Writes to Lean I/O channels are atomic, so these won't trample on each other. - o.writeLspMessage msg + else + -- Writes to Lean I/O channels are atomic, so these won't trample on each other. + o.writeLspMessage msg catch err => -- If writeLspMessage from above errors we will block here, but the main task will -- quit eventually anyways if that happens