michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/info_manager): get_closest_env_opts

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-18 17:03:59 -07:00
parent 9e29602934
commit b53b1825ae
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/frontends/lean/info_manager.cpp
View file

@ -590,7 +590,7 @@ struct info_manager::imp {
auto next = it;
next++;
if (next == m_env_info.end() || next->m_line > linenum)
return optional<pair<environment, options>>(mk_pair(it->m_env, it->m_options));
return optional<pair<environment, options>>(mk_pair(next->m_env, next->m_options));
it = next;
}
}