--- a/src/Tools/jEdit/src/rich_text_area.scala Thu Sep 20 21:57:37 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Thu Sep 20 22:25:30 2012 +0200
@@ -202,8 +202,8 @@
for { (color, separator) <- rendering.line_background(line_range) }
{
gfx.setColor(color)
- val tweak = if (separator) (2 min (line_height / 2)) else 0
- gfx.fillRect(0, y + i * line_height - tweak, text_area.getWidth, line_height - tweak)
+ val sep = if (separator) (2 min (line_height / 2)) else 0
+ gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
}
// background color (1)