diff options
| author | Maxime Coste <frrrwww@gmail.com> | 2013-11-18 22:43:37 +0000 |
|---|---|---|
| committer | Maxime Coste <frrrwww@gmail.com> | 2013-11-28 18:48:38 +0000 |
| commit | 2d55ff5febbb885c3b561d98a7723203cbca2c6e (patch) | |
| tree | 35f6f470f3501e4a9906d51bcc26a091c4919cdc /src/window.cc | |
| parent | fcf3e9e138c2089822527cfdeb04e706b6ee38d2 (diff) | |
Window: forget timestamp when options changes
Diffstat (limited to 'src/window.cc')
| -rw-r--r-- | src/window.cc | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/window.cc b/src/window.cc index eb26018a..d63e6bf0 100644 --- a/src/window.cc +++ b/src/window.cc @@ -253,6 +253,9 @@ void Window::on_option_changed(const Option& option) String desc = option.name() + "=" + option.get_as_string(); InputHandler hook_handler{*this}; m_hooks.run_hook("WinSetOption", desc, hook_handler.context()); + + // an highlighter might depend on the option, so we need to redraw + forget_timestamp(); } } |