author | wenzelm |
Mon, 20 Mar 2017 14:25:06 +0100 | |
changeset 65331 | 999864cdf96c |
parent 65329 | 4f3da52cec02 |
child 65332 | 7dbb780f24a9 |
--- a/src/Tools/jEdit/src/document_view.scala Sun Mar 19 20:28:21 2017 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Mon Mar 20 14:25:06 2017 +0100 @@ -213,7 +213,6 @@ val snapshot = model.snapshot() if (changed.assignment || - snapshot.commands_loading.exists(changed.commands.contains) || (changed.nodes.contains(model.node_name) && changed.commands.exists(snapshot.node.commands.contains))) text_overview.invoke()