# HG changeset patch
# User wenzelm
# Date 1332168987 -3600
# Node ID 95bd95addb24409cffec319661f6c14723086e52
# Parent  0e246130486b00705600db1508d74f094f1045f2
further amendment of "updated" edge (cf. 6ed49c52d463) -- required for repainting of unassigned command, e.g. for inactive buffe;

diff -r 0e246130486b -r 95bd95addb24 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Mon Mar 19 14:59:31 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Mar 19 15:56:27 2012 +0100
@@ -154,8 +154,8 @@
   {
     Swing_Thread.require()
     val snapshot = model.snapshot()
-    was_updated = was_outdated && !snapshot.is_outdated
-    was_outdated = was_outdated || snapshot.is_outdated
+    was_updated &&= !snapshot.is_outdated
+    was_outdated ||= snapshot.is_outdated
     snapshot
   }