diff -r 317077e35b0e -r 051cbf663b5f src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Fri Aug 23 11:23:26 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Fri Aug 23 11:41:17 2013 +0200
@@ -3,6 +3,9 @@
 public option jedit_logic : string = ""
   -- "default logic session"
 
+public option jedit_reset_font_size : int = 18
+  -- "reset font size for main text area"
+
 public option jedit_font_scale : real = 1.0
   -- "scale factor of add-on panels wrt. main text area"