From 2d55ff5febbb885c3b561d98a7723203cbca2c6e Mon Sep 17 00:00:00 2001
From: Maxime Coste <frrrwww@gmail.com>
Date: Mon, 18 Nov 2013 22:43:37 +0000
Subject: [PATCH] Window: forget timestamp when options changes

---
 src/window.cc | 3 +++
 1 file changed, 3 insertions(+)

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