michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/flycheck): crash when io_state_stream is destroyed before flycheck_scope

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-02 12:11:20 -08:00
parent 73429547ba
commit 1b13562591
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/flycheck.h
View file

@ -10,8 +10,8 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
/** \brief Auxiliary object for "inserting" delimiters for flycheck */ /** \brief Auxiliary object for "inserting" delimiters for flycheck */
class flycheck_scope { class flycheck_scope {
io_state_stream const & m_ios; io_state_stream m_ios;
bool m_flycheck; bool m_flycheck;
public: public:
flycheck_scope(io_state_stream const & ios, char const * kind); flycheck_scope(io_state_stream const & ios, char const * kind);
~flycheck_scope(); ~flycheck_scope();