max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/module_mgr): do not cause waits for preimported modules

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-04 17:50:21 +01:00 • committed by Leonardo de Moura
parent c9d2eeccf2
commit 96398500b6
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/module_mgr.cpp
View file

@ -96,6 +96,14 @@ public:
for (auto & d : m_deps)
if (d.m_mod_info)
deps.push_back(d.m_mod_info->m_result);
if (!m_deps.empty()) {
// also add the preimported environment of the first dependency
if (auto & mod_info = m_deps.front().m_mod_info) {
if (auto res = mod_info->m_result.peek()) {
deps.push_back(res->m_loaded_module->m_env);
}
}
}
return deps;
}