From beae2d936b00cedccb04997b2fce77c8762ff5f8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 May 2018 12:44:23 -0700 Subject: [PATCH] chore(library/init/lean/ir/parser): remove leftover --- library/init/lean/ir/parser.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/library/init/lean/ir/parser.lean b/library/init/lean/ir/parser.lean index b338efa1e4..3b7ea4dc10 100644 --- a/library/init/lean/ir/parser.lean +++ b/library/init/lean/ir/parser.lean @@ -126,5 +126,3 @@ def parse_instr : parser instr := end ir end lean - -#exit