From 1d524476b7ddfa391770e5b0caefe520f52bb980 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 12 Dec 2018 11:06:52 +0100
Subject: [PATCH] chore(tests/lean/parser1): restore `#exit`...

---
 tests/lean/parser1.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean
index 804d2366dc..0ec070a9df 100644
--- a/tests/lean/parser1.lean
+++ b/tests/lean/parser1.lean
@@ -137,6 +137,7 @@ def run_frontend (input : string) : except_t string io unit := do
   let stx := stx.update_leading input,
   io.println "result:",
   io.println (to_string stx)-/
+#exit
 
 -- slowly progressing...
 set_option profiler true