etc/options
changeset 57974 ba0b6c2338f0
parent 57867 abae8aff6262
child 58849 ef7700ecce83
     1.1 --- a/etc/options	Wed Aug 13 20:08:29 2014 +0200
     1.2 +++ b/etc/options	Wed Aug 13 20:21:04 2014 +0200
     1.3 @@ -138,6 +138,9 @@
     1.4  option editor_execution_delay : real = 0.02
     1.5    -- "delay for start of execution process after document update (seconds)"
     1.6  
     1.7 +option editor_syslog_limit : int = 100
     1.8 +  -- "maximum amount of buffered syslog messages"
     1.9 +
    1.10  
    1.11  section "Miscellaneous Tools"
    1.12