src/Tools/jEdit/src/plugin.scala
changeset 49272 97f8cb455691
parent 49250 332ab3748350
child 49288 2c9272cb4568
--- a/src/Tools/jEdit/src/plugin.scala	Tue Sep 11 15:59:35 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Sep 11 16:10:54 2012 +0200
@@ -58,8 +58,7 @@
   def font_family(): String = jEdit.getProperty("view.font")
 
   def font_size(): Float =
-    (jEdit.getIntegerProperty("view.fontsize", 16) *
-      options.int("jedit_relative_font_size")).toFloat / 100
+    (jEdit.getIntegerProperty("view.fontsize", 16) * options.real("jedit_font_scale")).toFloat
 
 
   /* tooltip markup */