# HG changeset patch
# User wenzelm
# Date 1450790795 -3600
# Node ID 30f70d1b97c97f8390050c820a483846482db6dd
# Parent  d5ddd4866b7b46227116b2ef587b60a625386011
more thorough event propagation;

diff -r d5ddd4866b7b -r 30f70d1b97c9 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Tue Dec 22 14:23:39 2015 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Tue Dec 22 14:26:35 2015 +0100
@@ -114,7 +114,8 @@
           val rendering = doc_view.get_rendering()
           val overview = get_overview()
 
-          if (!rendering.snapshot.is_outdated) {
+          if (rendering.snapshot.is_outdated) invoke()
+          else {
             cancel()
 
             val line_offsets =