| changeset 60292 | ba3c716144dd |
| parent 59390 | 7cab7fdf6048 |
| child 60847 | 239d7714392b |
--- a/src/Tools/jEdit/src/documentation_dockable.scala Tue May 19 18:34:16 2015 +0200 +++ b/src/Tools/jEdit/src/documentation_dockable.scala Wed May 20 22:22:27 2015 +0200 @@ -46,6 +46,7 @@ } private val tree = new JTree(root) + tree.setRowHeight(0) override def focusOnDefaultComponent { tree.requestFocusInWindow }