changeset 39516 | 8a70e91650a6 |
parent 37067 | 31093f3687b5 |
child 39588 | 507fcf86e1e0 |
--- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala Sat Sep 18 14:28:42 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala Sat Sep 18 15:50:29 2010 +0200 @@ -19,6 +19,7 @@ extends Dockable(view: View, position: String) { private val text_area = new TextArea + text_area.editable = false set_content(new ScrollPane(text_area))