changeset 57595 | e2305b9d1534 |
parent 57594 | 037f3b251df5 |
child 57691 | 9616643a3032 |
--- a/src/Tools/jEdit/src/rendering.scala Mon Jul 21 17:37:22 2014 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Mon Jul 21 17:39:20 2014 +0200 @@ -149,7 +149,7 @@ private val active_elements = Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, - Markup.SENDBACK, Markup.SIMP_TRACE, Markup.SIMP_TRACE_PANEL) + Markup.SENDBACK, Markup.SIMP_TRACE_PANEL) private val tooltip_message_elements = Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)