author | wenzelm |
Tue, 15 Sep 2009 20:39:00 +0200 | |
changeset 34735 | 2997f2a0f831 |
parent 34734 | 02479f4ac9a5 |
child 34736 | ff7734c8bdb7 |
--- 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) "<html><b>TODO:</b><br>Tooltip</html>" else "" }