changeset 61023 | 46df28442a80 |
parent 61011 | 018b0c996b54 |
child 61139 | f9fd43d8981d |
--- a/src/Tools/jEdit/etc/options Tue Aug 25 10:41:12 2015 +0200 +++ b/src/Tools/jEdit/etc/options Tue Aug 25 13:46:24 2015 +0200 @@ -9,7 +9,7 @@ public option jedit_auto_load : bool = false -- "load all required files automatically to resolve theory imports" -public option jedit_auto_resolve : bool = false +public option jedit_auto_resolve : bool = true -- "automatically resolve auxiliary files within the editor" public option jedit_reset_font_size : int = 18