From b2fda9b9ae43d46b412007ba6df3abd20debb740 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 25 Dec 2020 18:48:58 +0100
Subject: [PATCH] chore: disable randomly failing test

/cc @mhuisi @Vtech234
---
 tests/lean/server/init_exit.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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)
+-/