fix(frontends/lean/module_parser): make the #exit command end at the end of the file

Fixes #1553.
This commit is contained in:
Gabriel Ebner 2017-05-01 13:22:26 +02:00
parent e6a62b8030
commit 3e2e9ed98a

View file

@ -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;