From 87926b774fdace1cd5a757f27908e7919ed07f20 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 1 Sep 2014 18:42:46 -0700 Subject: [PATCH] fix(frontends/lean/info_manager): user provided options override saved options, fixes #119 Signed-off-by: Leonardo de Moura --- src/frontends/lean/info_manager.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 8b5947d38..ad0937d95 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -454,7 +454,7 @@ struct info_manager::imp { auto next = it; ++next; 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; } it = next;