From 1b135625913a281f22cfb0644f267f33a352fcb8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 2 Dec 2014 12:11:20 -0800 Subject: [PATCH] fix(library/flycheck): crash when io_state_stream is destroyed before flycheck_scope --- src/library/flycheck.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/flycheck.h b/src/library/flycheck.h index fcac082b1..f7551ee25 100644 --- a/src/library/flycheck.h +++ b/src/library/flycheck.h @@ -10,8 +10,8 @@ Author: Leonardo de Moura namespace lean { /** \brief Auxiliary object for "inserting" delimiters for flycheck */ class flycheck_scope { - io_state_stream const & m_ios; - bool m_flycheck; + io_state_stream m_ios; + bool m_flycheck; public: flycheck_scope(io_state_stream const & ios, char const * kind); ~flycheck_scope();