# HG changeset patch # User wenzelm # Date 1253039940 -7200 # Node ID 2997f2a0f8314871931a0148673f08b55a8e4950 # Parent 02479f4ac9a5b397c4c4181c6bbd4f0a999a2371 tooltip: HTML dummy; diff -r 02479f4ac9a5 -r 2997f2a0f831 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Tue Sep 15 20:30:17 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Tue Sep 15 20:39:00 2009 +0200 @@ -52,7 +52,7 @@ val buffer = text_area.getBuffer val lineCount = buffer.getLineCount val line = y_to_line(event.getY()) - if (line >= 0 && line < text_area.getLineCount) "TODO: Tooltip" + if (line >= 0 && line < text_area.getLineCount) "TODO:
Tooltip" else "" }