Window: forget timestamp when options changes

This commit is contained in:
Maxime Coste 2013-11-18 22:43:37 +00:00
parent fcf3e9e138
commit 2d55ff5feb

View File

@ -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();
}
}