author | wenzelm |
Tue, 26 Mar 2013 14:03:31 +0100 | |
changeset 51535 | f2f480bc4223 |
parent 51534 | 123bd97fcea1 |
child 51536 | a1d324ef12d4 |
--- a/src/Tools/jEdit/src/theories_dockable.scala Tue Mar 26 12:40:51 2013 +0100 +++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Mar 26 14:03:31 2013 +0100 @@ -93,7 +93,7 @@ (st.failed, PIDE.options.color_value("error_color"))) val size = peer.getSize() - val insets = border.getBorderInsets(this.peer) + val insets = border.getBorderInsets(peer) val w = size.width - insets.left - insets.right val h = size.height - insets.top - insets.bottom var end = size.width - insets.right