From 2ca347fcd622a5a1dce4b3dd3a2486c366bf54b5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Mar 2020 15:47:51 -0700
Subject: [PATCH] chore: fix test

---
 tests/lean/run/getline_crash.lean | 21 +++++++--------------
 1 file changed, 7 insertions(+), 14 deletions(-)

diff --git a/tests/lean/run/getline_crash.lean b/tests/lean/run/getline_crash.lean
index 62445b3ed2..a98170c8e8 100644
--- a/tests/lean/run/getline_crash.lean
+++ b/tests/lean/run/getline_crash.lean
@@ -29,26 +29,19 @@ IO.FS.withFile path IO.FS.Mode.read $ λ (h : IO.FS.Handle) => do
   unless (str2'.trim == str2) $
     throw (IO.userError ("unexpected result: " ++ str2'))
 
-def tstGetLineFailure1 (str : String) : IO Unit := do
+def tstGetLine3 (str : String) : IO Unit := do
 let path := "tmp_file";
 IO.FS.withFile path IO.FS.Mode.write $ λ (h : IO.FS.Handle) => do {
   h.putStrLn str
 };
 IO.FS.withFile path IO.FS.Mode.read $ λ (h : IO.FS.Handle) => do
-  whenM (catch (do (h.getLine >>= IO.println); (h.getLine >>= IO.println); (h.getLine >>= IO.println); pure true) (fun _ => pure false)) $
-    throw $ IO.userError "unexpected success"
+  (h.getLine >>= IO.println);
+  (h.getLine >>= IO.println);
+  (h.getLine >>= IO.println);
+  IO.print "done";
+  pure ()
 
-def tstGetLineFailure2 (str : String) : IO Unit := do
-let path := "tmp_file";
-IO.FS.withFile path IO.FS.Mode.write $ λ (h : IO.FS.Handle) => do {
-  h.putStrLn str
-};
-IO.FS.withFile path IO.FS.Mode.read $ λ (h : IO.FS.Handle) => do
-  whenM (catch (do (h.getLine >>= IO.println); (h.getLine >>= IO.println); pure true) (fun _ => pure false)) $
-    throw $ IO.userError "unexpected success"
-
-#eval tstGetLineFailure1 "abc"
-#eval tstGetLineFailure2 "abc"
+#eval tstGetLine3 "abc"
 
 #eval tstGetLine ("".pushn 'α' 40)
 #eval tstGetLine "a"