--- a/src/Tools/jEdit/patches/render_context Sun Mar 04 19:24:05 2012 +0100
+++ /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();
-