From 42642a2890d5786a209f61b464dccc19ecb0dcd6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Jan 2020 16:13:32 -0800 Subject: [PATCH] fix: `new_frontend` command issue --- src/frontends/lean/util.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 4a700a136b..e269feb99c 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -55,7 +55,7 @@ void consume_until_end_or_command(parser & p) { void check_command_period_docstring_or_eof(parser const & p) { if (!p.curr_is_command() && !p.curr_is_eof() && !p.curr_is_token(get_period_tk()) && - p.curr() != token_kind::DocBlock && p.curr() != token_kind::ModDocBlock) + p.curr() != token_kind::DocBlock && p.curr() != token_kind::ModDocBlock && p.curr() != token_kind::NewFrontend) throw parser_error("unexpected token, '.', command, or end-of-file expected", p.pos()); }