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  

     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 13 20:08:29 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 13 20:21:04 2014 +0200
     2.3 @@ -392,6 +392,7 @@
     2.4        PIDE.session = new Session(resources) {
     2.5          override def output_delay = PIDE.options.seconds("editor_output_delay")
     2.6          override def prune_delay = PIDE.options.seconds("editor_prune_delay")
     2.7 +        override def syslog_limit = PIDE.options.int("editor_syslog_limit")
     2.8          override def reparse_limit = PIDE.options.int("editor_reparse_limit")
     2.9        }
    2.10