From 06002c5312366e7b5c5e247af153dd3361cf2b4a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Jun 2014 22:09:42 -0700 Subject: [PATCH] feat(frontends/lean/parser): use system_import when processing Lean import command Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 0c2da6070..4267da268 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -989,11 +989,8 @@ void parser::parse_imports() { } } m_env = import_modules(m_env, olean_files.size(), olean_files.data(), m_num_threads, true, m_ios); - using_script([&](lua_State * L) { - for (auto const & f : lua_files) { - to_script_state(L).import_explicit(f.c_str()); - } - }); + for (auto const & f : lua_files) + system_import(f.c_str()); } bool parser::parse_commands() {