# HG changeset patch
# User wenzelm
# Date 1407954064 -7200
# Node ID ba0b6c2338f0a603ba546371eac780e5e60a9233
# Parent  decf2e9289ab7a6f489b0c7a79c46b0b35eb2ab4
added option editor_syslog_limit;

diff -r decf2e9289ab -r ba0b6c2338f0 etc/options
--- 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"
 
diff -r decf2e9289ab -r ba0b6c2338f0 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 13 20:08:29 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 13 20:21:04 2014 +0200
@@ -392,6 +392,7 @@
       PIDE.session = new Session(resources) {
         override def output_delay = PIDE.options.seconds("editor_output_delay")
         override def prune_delay = PIDE.options.seconds("editor_prune_delay")
+        override def syslog_limit = PIDE.options.int("editor_syslog_limit")
         override def reparse_limit = PIDE.options.int("editor_reparse_limit")
       }