--- a/src/Tools/jEdit/patches/gutter Sun Mar 19 18:28:32 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-diff -ru 5.3.0/jEdit-orig/org/gjt/sp/jedit/textarea/Gutter.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/Gutter.java
---- 5.3.0/jEdit-orig/org/gjt/sp/jedit/textarea/Gutter.java 2015-10-20 19:56:03.000000000 +0200
-+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/Gutter.java 2015-11-24 21:58:47.686343684 +0100
-@@ -185,8 +185,6 @@
- }
-
- int y = clip.y - clip.y % lineHeight;
-- if (y == 0)
-- y = textArea.getPainter().getLineExtraSpacing();
-
- extensionMgr.paintScreenLineRange(textArea,gfx,
- firstLine,lastLine,y,lineHeight);
-@@ -725,7 +723,7 @@
-
- FontMetrics textAreaFm = textArea.getPainter().getFontMetrics();
- int lineHeight = textArea.getPainter().getLineHeight();
-- int baseline = textAreaFm.getAscent();
-+ int baseline = lineHeight - (textAreaFm.getLeading()+1) - textAreaFm.getDescent();
-
- ChunkCache.LineInfo info = textArea.chunkCache.getLineInfo(line);
- int physicalLine = info.physicalLine;