changeset 54881 | dff57132cf18 |
parent 54377 | 750561986828 |
child 55033 | 8e8243975860 |
--- a/src/Tools/jEdit/etc/options Mon Dec 30 12:58:13 2013 +0100 +++ b/src/Tools/jEdit/etc/options Mon Dec 30 20:35:17 2013 +0100 @@ -3,6 +3,9 @@ public option jedit_logic : string = "" -- "default logic session" +public option jedit_print_mode : string = "" + -- "default print modes for output, separated by commas (change requires restart)" + public option jedit_auto_load : bool = false -- "load all required files automatically to resolve theory imports"