| changeset 61726 | 04f8564d6983 |
| parent 61721 | e37046b121a2 |
| child 61801 | fa8d1cdf6518 |
--- a/src/Tools/jEdit/src/state_dockable.scala Sat Nov 21 19:27:06 2015 +0100 +++ b/src/Tools/jEdit/src/state_dockable.scala Sat Nov 21 19:38:14 2015 +0100 @@ -57,7 +57,7 @@ /* update */ - private var do_update = false + private var do_update = true private def maybe_update(): Unit = GUI_Thread.require { if (do_update) update() }