From 75be034d3dbb04d8c860a40025a195c2337a741b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Aug 2014 18:31:47 -0700 Subject: [PATCH] fix(frontends/lean/server): crash when INFO is invoked before VISIT/LOAD Signed-off-by: Leonardo de Moura --- src/frontends/lean/server.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 584c933db..63d7f2b36 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -150,6 +150,7 @@ void server::visit_file(std::string const & fname) { } void server::show_info(unsigned linenum) { + check_file(); update(); unsigned i = m_file->find(linenum); environment const & env = i == 0 ? m_env : m_file->m_snapshots[i-1].m_env;