diff -r 80c432404204 -r 9fc17f9ccd6c src/Tools/jEdit/patches/jedit-4.4.1/render_context
--- a/src/Tools/jEdit/patches/jedit-4.4.1/render_context	Tue Mar 27 22:10:26 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-diff -ru 4.4.1/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java
---- 4.4.1/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2011-06-21 01:28:56.000000000 +0200
-+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2011-06-22 16:18:43.000000000 +0200
-@@ -646,7 +646,7 @@
- 			this.font = font;
- 
- 			FontRenderContext fontRenderContext
--				= new FontRenderContext(null,true,true);
-+				= new FontRenderContext(null,true,false);
- 			glyphs = font.createGlyphVector(fontRenderContext,text);
- 			width = (int)glyphs.getLogicalBounds().getWidth() + 4;
- 			//height = (int)glyphs.getLogicalBounds().getHeight();
-