Skip to content

Commit

Permalink
fix: lsp
Browse files Browse the repository at this point in the history
  • Loading branch information
tonyxty authored and alissa-tung committed Dec 23, 2023
1 parent 7c38649 commit e16e139
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion src/Lean/Server/Watchdog.lean
Original file line number Diff line number Diff line change
Expand Up @@ -661,7 +661,6 @@ def mkLeanServerCapabilities : ServerCapabilities := {
def initAndRunWatchdogAux : ServerM Unit := do
let st ← read
try
discard $ st.hIn.readLspNotificationAs "initialized" InitializedParams
let clientTask ← runClientTask
mainLoop clientTask
catch err =>
Expand Down

0 comments on commit e16e139

Please sign in to comment.