diff -r e23e0ff98657 -r 3df1b6a5837c src/Tools/jEdit/patches/gutter
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/gutter	Tue Nov 24 22:50:03 2015 +0100
@@ -0,0 +1,21 @@
+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;