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

fix(library/module_mgr): do not perform unnecessary copy

Browse source
This commit is contained in:
Gabriel Ebner 2016-12-12 11:06:45 -05:00 • committed by Leonardo de Moura
parent 028bf36152
commit cf3f398753
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/module_mgr.cpp
View file

@ -61,7 +61,7 @@ public:
module_info::parse_result execute() override {
module_loader import_fn = [=] (module_id const & base, module_name const & import) {
for (auto d : m_deps) {
for (auto & d : m_deps) {
if (std::get<0>(d) == base &&
std::get<1>(d).m_name == import.m_name &&
std::get<1>(d).m_relative == import.m_relative) {