# HG changeset patch
# User wenzelm
# Date 1252845290 -7200
# Node ID 43b02b4c8e0b812777e5ec2d07d2f3c91c7e6d62
# Parent  b1079c3ba1da0f26742f54d68a1bc5d70f5ed9a3
avoid fractional font metrics, which produces bad antialiasing with reletively new versions of jedit and java;

diff -r b1079c3ba1da -r 43b02b4c8e0b src/Tools/jEdit/dist-template/properties/jedit.props
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Sep 08 22:38:01 2009 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Sun Sep 13 14:34:50 2009 +0200
@@ -186,7 +186,7 @@
 view.extendedState=0
 view.font=Lucida Sans Typewriter
 view.fontsize=18
-view.fracFontMetrics=true
+view.fracFontMetrics=false
 view.gutter.fontsize=12
 view.middleMousePaste=true
 view.showToolbar=false