author | wenzelm |
Wed, 19 Aug 2015 15:40:59 +0200 | |
changeset 60973 | d94f3afd69b6 |
parent 60972 | 4fc468197040 |
child 60974 | 6a6f15d8fbc4 |
child 60975 | 5f3d6e16ea78 |
--- a/src/Tools/jEdit/etc/options Tue Aug 18 17:06:34 2015 +0200 +++ b/src/Tools/jEdit/etc/options Wed Aug 19 15:40:59 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 = true +public option jedit_auto_resolve : bool = false -- "automatically resolve auxiliary files within the editor" public option jedit_reset_font_size : int = 18