From 4b604521a0730948bc4236d4090e336aa98cf77f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 Aug 2014 16:26:04 -0700 Subject: [PATCH] fix(frontends/lean): add hack for flycheck Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index b8ec7ad255..bd229b4664 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1257,7 +1257,7 @@ public: if (!prev || p.first != prev->first) { auto out = regular(m_env, m_ios); flyinfo_scope info(out); - out << m_pos_provider->get_file_name() << ":" << p.first.first << ":" << p.first.second + out << m_pos_provider->get_file_name() << ":" << p.first.first << ":" << p.first.second+1 << ": type\n" << p.second << endl; prev = p; }