diff --git a/tests/lean/server/init_exit.lean b/tests/lean/server/init_exit.lean index fa8e65e0f1..336245ba71 100644 --- a/tests/lean/server/init_exit.lean +++ b/tests/lean/server/init_exit.lean @@ -1,6 +1,7 @@ import Lean.Data.Lsp open IO Lean Lsp +/- #eval (do Ipc.runWith (←IO.appPath) #["--server"] do let hIn ← Ipc.stdin @@ -14,4 +15,5 @@ open IO Lean Lsp let shutdownResp ← Ipc.readResponseAs 1 Json assert! shutdownResp.result.isNull Ipc.writeNotification ⟨"exit", Json.null⟩ - : IO Unit) \ No newline at end of file + : IO Unit) +-/