src/Tools/jEdit/src/rich_text_area.scala

--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Jul 01 14:37:31 2013 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Jul 01 14:56:10 2013 +0200
@@ -213,7 +213,7 @@
                         val screen_point = e.getLocationOnScreen
                         screen_point.translate(0, painter.getFontMetrics.getHeight / 2)
                         val results = rendering.command_results(range)
-                        Pretty_Tooltip(view, painter, rendering, screen_point, results, tip.info)
+                        Pretty_Tooltip(view, painter, rendering, screen_point, results, tip)
                     }
                 }
               }