diff options
| author | Maxime Coste <frrrwww@gmail.com> | 2016-03-03 13:55:35 +0000 |
|---|---|---|
| committer | Maxime Coste <frrrwww@gmail.com> | 2016-03-03 14:05:07 +0000 |
| commit | b5b5b82c70533c833396fbe490e860d4820ca022 (patch) | |
| tree | 63c2a604017fe65bdde1f126715716f8193b7f7d /src/client_manager.hh | |
| parent | f16bb36f41432c0938954d0e42f57eedf8ed0287 (diff) | |
destroy buffer manager first but clear clients before destroying buffers.
Fixes #612
Diffstat (limited to 'src/client_manager.hh')
| -rw-r--r-- | src/client_manager.hh | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/client_manager.hh b/src/client_manager.hh index cd7f12bf..c6ba1c35 100644 --- a/src/client_manager.hh +++ b/src/client_manager.hh @@ -33,6 +33,8 @@ public: bool empty() const { return m_clients.empty(); } size_t count() const { return m_clients.size(); } + void clear(); + void ensure_no_client_uses_buffer(Buffer& buffer); WindowAndSelections get_free_window(Buffer& buffer); |