changeset 68197 | 7857817403e4 |
parent 68184 | 6c693b2700b3 |
child 68221 | dbef88c2b6c5 |
--- a/etc/options Wed May 16 21:06:28 2018 +0200 +++ b/etc/options Wed May 16 21:07:12 2018 +0200 @@ -189,8 +189,8 @@ option editor_syslog_limit : int = 100 -- "maximum amount of buffered syslog messages" -public option editor_document_output : bool = false - -- "dynamic document output while editing" +public option editor_presentation : bool = false + -- "dynamic presentation while editing" section "Miscellaneous Tools"