# HG changeset patch
# User wenzelm
# Date 1472830512 -7200
# Node ID 749794930d618f6edc46126d83a79283216c84aa
# Parent  d1a5d10affc05d20958eb4f81f80ac5664be6a26
make double-sure that refresh happens eventually, even without edits (e.g. height change) -- amending 8bf765c9c2e5;

diff -r d1a5d10affc0 -r 749794930d61 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Fri Sep 02 16:23:02 2016 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala	Fri Sep 02 17:35:12 2016 +0200
@@ -86,6 +86,7 @@
         val overview = get_overview()
 
         if (rendering.snapshot.is_outdated || overview != current_overview) {
+          invoke()
           delay_repaint.invoke()
 
           gfx.setColor(rendering.outdated_color)