changeset 73367 | 77ef8bef0593 |
parent 73358 | 78aa7846e91f |
child 73413 | 56c0a793cd8b |
--- a/src/Tools/jEdit/src/document_model.scala Thu Mar 04 19:55:52 2021 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Thu Mar 04 21:04:27 2021 +0100 @@ -592,7 +592,7 @@ val edits = get_edits val (reparse, perspective) = node_perspective(doc_blobs, hidden) if (reparse || edits.nonEmpty || last_perspective != perspective) { - pending.clear + pending.clear() last_perspective = perspective node_edits(node_header(), edits, perspective) }