changeset 1057 | 3837e165b3f9 |
parent 1042 | 6dbdc6844eb9 |
child 1069 | 880ec628d490 |
--- a/editors/Viewer.py Tue Apr 23 23:02:35 2013 +0200 +++ b/editors/Viewer.py Wed Apr 24 00:20:13 2013 +0200 @@ -3167,6 +3167,7 @@ blocks.append((block, (infos[1:], start, end, SEARCH_RESULT_HIGHLIGHT))) blocks.sort(sort_blocks) self.SearchResults.extend([infos for block, infos in blocks]) + self.CurrentFindHighlight = None if len(self.SearchResults) > 0: if self.CurrentFindHighlight is not None: