author | wenzelm |
Sat, 15 Dec 2012 12:01:07 +0100 | |
changeset 50541 | 021f054ff1fa |
parent 50540 | f4aac67a6405 |
child 50542 | 58bd88159f8f |
--- 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)