--- a/src/Pure/PIDE/session.scala Tue Aug 05 19:58:07 2014 +0200
+++ b/src/Pure/PIDE/session.scala Tue Aug 05 20:40:35 2014 +0200
@@ -176,7 +176,7 @@
/* tuning parameters */
def output_delay: Time = Time.seconds(0.1) // prover output (markup, common messages)
- def prune_delay: Time = Time.seconds(60.0) // prune history -- delete old versions
+ def prune_delay: Time = Time.seconds(60.0) // prune history (delete old versions)
def prune_size: Int = 0 // size of retained history
def syslog_limit: Int = 100
def reparse_limit: Int = 0