src/Tools/jEdit/src/jedit/plugin.scala

--- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu May 20 23:19:28 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu May 20 23:20:01 2010 +0200
@@ -70,8 +70,9 @@
       jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
   }
 
-  def font_size(): Int =
-    (jEdit.getIntegerProperty("view.fontsize", 16) * Int_Property("relative-font-size", 100)) / 100
+  def font_size(): Float =
+    (jEdit.getIntegerProperty("view.fontsize", 16) *
+      Int_Property("relative-font-size", 100)).toFloat / 100
 
 
   /* settings */