max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: don't send worker notification to client

Browse source
This commit is contained in:
Joscha 2022-01-19 16:07:41 +01:00 • committed by Sebastian Ullrich
parent 89e460dd1b
commit 3651ebb377
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Server/Watchdog.lean
View file

@ -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