changeset 60916 | a6e2a667b0a8 |
parent 60914 | f39d004f2ff4 |
child 60973 | d94f3afd69b6 |
--- a/src/Tools/jEdit/etc/options Wed Aug 12 03:07:01 2015 +0200 +++ b/src/Tools/jEdit/etc/options Wed Aug 12 13:53:51 2015 +0200 @@ -9,6 +9,9 @@ public option jedit_auto_load : bool = false -- "load all required files automatically to resolve theory imports" +public option jedit_auto_resolve : bool = true + -- "automatically resolve auxiliary files within the editor" + public option jedit_reset_font_size : int = 18 -- "reset main text font size"