# HG changeset patch
# User wenzelm
# Date 1307966021 -7200
# Node ID df1be524e60c43841e85e1ae97b7e2a21fdc6944
# Parent  639c3aca2ed32d10bfd8d5a112a518d4016cdf41
tuned;

diff -r 639c3aca2ed3 -r df1be524e60c src/Tools/jEdit/src/text_painter.scala
--- 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)