changeset 50501 | 6f41f1646617 |
parent 50452 | bfb5964e3041 |
child 50507 | 9605b0d93d1e |
--- a/src/Tools/jEdit/src/graphview_dockable.scala Thu Dec 13 13:52:18 2012 +0100 +++ b/src/Tools/jEdit/src/graphview_dockable.scala Thu Dec 13 17:29:23 2012 +0100 @@ -65,7 +65,7 @@ override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = { val rendering = Rendering(snapshot, PIDE.options.value) - new Pretty_Tooltip(view, parent, rendering, x, y, body) + new Pretty_Tooltip(view, parent, rendering, x, y, Command.empty_results, body) null } }