From 0ca0ccb77d416f41f47a747d8ae854789f2ea1b6 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 12 Aug 2014 17:09:59 -0700
Subject: [PATCH] feat(frontend/lean/server.cpp): add "-- BEGININFO" header

---
 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 0d68adf947..c1e37c3c23 100644
--- a/src/frontends/lean/server.cpp
+++ b/src/frontends/lean/server.cpp
@@ -156,6 +156,7 @@ void server::show_info(unsigned linenum) {
     options const & o       = i == 0 ? m_options : m_file->m_snapshots[i-1].m_options;
     m_ios.set_options(o);
     io_state_stream out(env, m_ios);
+    out << "-- BEGININFO" << endl;
     m_file->m_info.display(out, linenum);
     out << "-- ENDINFO" << endl;
 }