changeset 56931 | 9ecf2cbfc80d |
parent 56918 | a442dc6d244d |
child 57042 | 5576d22abf3c |
--- a/src/Tools/jEdit/src/output_dockable.scala Fri May 09 21:02:15 2014 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Fri May 09 21:03:44 2014 +0200 @@ -20,9 +20,6 @@ class Output_Dockable(view: View, position: String) extends Dockable(view, position) { - override def focusOnDefaultComponent { view.getTextArea.requestFocus } - - /* component state -- owned by Swing thread */ private var zoom_factor = 100