From 3e2e9ed98af19c1ae79abc7c716158d46aec491a Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 1 May 2017 13:22:26 +0200
Subject: [PATCH] fix(frontends/lean/module_parser): make the #exit command end
 at the end of the file

Fixes #1553.
---
 src/frontends/lean/module_parser.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/frontends/lean/module_parser.cpp b/src/frontends/lean/module_parser.cpp
index f1d4dbdf3e..95f1fca1c9 100644
--- a/src/frontends/lean/module_parser.cpp
+++ b/src/frontends/lean/module_parser.cpp
@@ -91,6 +91,7 @@ task<module_parser_result> module_parser::parse_next_command_like(optional<std::
             done = true;
         }
         auto end_pos = self->m_parser.pos();
+        if (done) end_pos = self->m_end_pos;
         lean_assert(end_pos >= begin_pos);
 
         module_parser_result res;