src/Tools/jEdit/src/plugin.scala
changeset 57979 fc136831d6ca
parent 57908 1937603dbdf2
parent 57974 ba0b6c2338f0
child 58928 23d0ffd48006
--- a/src/Tools/jEdit/src/plugin.scala	Sun Aug 17 22:27:58 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 18 13:19: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")
       }