changeset 50541 | 021f054ff1fa |
parent 50501 | 6f41f1646617 |
child 50773 | 205d12333fdc |
--- a/src/Tools/jEdit/src/output_dockable.scala Fri Dec 14 23:04:35 2012 +0100 +++ b/src/Tools/jEdit/src/output_dockable.scala Sat Dec 15 12:01:07 2012 +0100 @@ -37,7 +37,7 @@ /* pretty text area */ - private val pretty_text_area = new Pretty_Text_Area(view) + val pretty_text_area = new Pretty_Text_Area(view) set_content(pretty_text_area)