# HG changeset patch # User wenzelm # Date 1355569267 -3600 # Node ID 021f054ff1faedb0922d7c59084c06e9fb00a90c # Parent f4aac67a6405a5553f831f5db78d50246582f58f tuned signature; diff -r f4aac67a6405 -r 021f054ff1fa src/Tools/jEdit/src/output_dockable.scala --- 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)