--- a/src/Tools/jEdit/etc/options Tue Sep 11 15:59:35 2012 +0200
+++ b/src/Tools/jEdit/etc/options Tue Sep 11 16:10:54 2012 +0200
@@ -6,8 +6,8 @@
option jedit_auto_start : bool = true
-- "auto-start prover session on editor startup"
-option jedit_relative_font_size : int = 100
- -- "relative font size of output panel wrt. main text area"
+option jedit_font_scale : real = 1.0
+ -- "scale factor of add-on panels wrt. main text area"
option jedit_tooltip_font_size : int = 10
-- "tooltip font size (according to HTML)"