author | wenzelm |
Tue, 08 Sep 2015 21:57:18 +0200 | |
changeset 61139 | f9fd43d8981d |
parent 61138 | dcbec1b22b07 |
child 61141 | 92858a52e45b |
child 61142 | 6d29eb7c5fb2 |
--- a/src/Tools/jEdit/etc/options Tue Sep 08 21:49:21 2015 +0200 +++ b/src/Tools/jEdit/etc/options Tue Sep 08 21:57:18 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