From 1dfc21efcc193a283550784858e54ab34bcd6167 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 25 May 2023 18:18:21 -0400 Subject: [PATCH] fix: use a less ambiguous encoding for relative imports --- src/frontends/lean/parser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 8c7e23f29c..539db6b930 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2721,7 +2721,7 @@ bool parser::parse_imports(unsigned & fingerprint, ast_data * parent, std::vecto auto& ast_mod = new_ast("module", p); import_cmd.push(ast_mod.m_id); if (k_init) { - ast_mod.m_value = f.append_after(k); + ast_mod.m_value = name(f, k); module_name m(f, k); imports.push_back(m); } else {