| changeset 60750 | 7694aa52ad56 |
| parent 60278 | 2a9bc6447779 |
| child 60861 | fa77faa87d5f |
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Jul 17 21:40:47 2015 +0200 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Jul 17 21:45:15 2015 +0200 @@ -66,6 +66,7 @@ addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } + override def componentShown(e: ComponentEvent) { delay_resize.invoke() } })