equal
deleted
inserted
replaced
|
1 diff -ru jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java |
|
2 --- jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2010-05-09 14:29:17.000000000 +0200 |
|
3 +++ jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2011-06-21 23:00:11.000000000 +0200 |
|
4 @@ -646,7 +646,7 @@ |
|
5 this.font = font; |
|
6 |
|
7 FontRenderContext fontRenderContext |
|
8 - = new FontRenderContext(null,true,true); |
|
9 + = new FontRenderContext(null,true,false); |
|
10 glyphs = font.createGlyphVector(fontRenderContext,text); |
|
11 width = (int)glyphs.getLogicalBounds().getWidth() + 4; |
|
12 //height = (int)glyphs.getLogicalBounds().getHeight(); |