etc/options
changeset 68184 6c693b2700b3
parent 68154 42d63ea39161
child 68197 7857817403e4
     1.1 --- a/etc/options	Mon May 14 22:01:00 2018 +0200
     1.2 +++ b/etc/options	Mon May 14 22:22:47 2018 +0200
     1.3 @@ -189,6 +189,9 @@
     1.4  option editor_syslog_limit : int = 100
     1.5    -- "maximum amount of buffered syslog messages"
     1.6  
     1.7 +public option editor_document_output : bool = false
     1.8 +  -- "dynamic document output while editing"
     1.9 +
    1.10  
    1.11  section "Miscellaneous Tools"
    1.12