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") }