changeset 50507 | 9605b0d93d1e |
parent 50501 | 6f41f1646617 |
child 51449 | 8d6e478934dc |
--- a/src/Tools/jEdit/src/graphview_dockable.scala Thu Dec 13 19:53:55 2012 +0100 +++ b/src/Tools/jEdit/src/graphview_dockable.scala Fri Dec 14 12:09:08 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, Command.empty_results, body) + new Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body) null } }