# 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 ""
}