avoid fractional font metrics, which produces bad antialiasing with reletively new versions of jedit and java;

--- 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