author | wenzelm |
Tue, 22 Dec 2015 14:26:35 +0100 | |
changeset 61904 | 30f70d1b97c9 |
parent 61903 | d5ddd4866b7b |
child 61905 | ea79448eb426 |
--- 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 =