From e0ae6068d44760bbc7d5cf54fcac4ef0c03421d7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Jan 2020 21:00:52 -0800 Subject: [PATCH] chore: set `end_pos` --- src/frontends/lean/parser.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 3b1a3e8a31..3904be2e32 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2141,7 +2141,9 @@ void parser::parse_new_frontend_cmd() { pos.first += curr_pos.first; message_severity sev = get_message_severity(msg); std::string str = get_message_string(msg); - auto builder = mk_message(pos, sev); + pos_info end_pos = pos; // retrieve message end_pos + end_pos.second += 1; + auto builder = mk_message(pos, end_pos, sev); builder << str; builder.report(); }