--- a/src/Tools/jEdit/src/text_painter.scala Mon Jun 13 12:33:53 2011 +0200
+++ b/src/Tools/jEdit/src/text_painter.scala Mon Jun 13 13:53:41 2011 +0200
@@ -81,7 +81,6 @@
line_infos.get(start(i)) match {
case Some(chunk) =>
val w = Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR).toInt
- gfx.setFont(font)
gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
orig_text_painter.paintValidLine(
gfx, first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)