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