etc/options
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"