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

fix(frontends/lean/info_manager): user provided options override saved options, fixes #119

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-01 18:42:46 -07:00
parent 50465a2d06
commit 87926b774f
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

@ -454,7 +454,7 @@ struct info_manager::imp {
auto next = it; auto next = it;
++next; ++next;
if (next == end || next->m_line > line) { if (next == end || next->m_line > line) {
display_core(it->m_env, it->m_options, ios, line); display_core(it->m_env, join(it->m_options, ios.get_options()), ios, line);
return; return;
} }
it = next; it = next;