| author | wenzelm | 
| Sat, 21 Nov 2015 16:07:29 +0100 | |
| changeset 61721 | e37046b121a2 | 
| parent 61720 | a31730632e13 | 
| child 61722 | a8fb3e379ba7 | 
--- a/src/Tools/jEdit/src/state_dockable.scala Sat Nov 21 16:06:36 2015 +0100 +++ b/src/Tools/jEdit/src/state_dockable.scala Sat Nov 21 16:07:29 2015 +0100 @@ -57,7 +57,7 @@ /* update */ - private var do_update = true + private var do_update = false private def maybe_update(): Unit = GUI_Thread.require { if (do_update) update() }