changeset 81398 | f92ea68473f2 |
parent 81340 | 30f7eb65d679 |
child 82142 | 508a673c87ac |
--- a/src/Tools/Graphview/graphview.scala Thu Nov 07 20:43:25 2024 +0100 +++ b/src/Tools/Graphview/graphview.scala Fri Nov 08 13:27:26 2024 +0100 @@ -85,7 +85,7 @@ /* tooltips */ - def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null + def make_tooltip(parent: JComponent, x: Int, y: Int, tip: XML.Elem): String = null /* main colors */