# HG changeset patch
# User wenzelm
# Date 1450563923 -3600
# Node ID 7e8f4df04d5dd37da8c66cad88433a0eebedd9af
# Parent  fcb4d24c384c5beb32abe863e2d9c11e06052768
prune old document versions more frequently, for reduced heap usage;

diff -r fcb4d24c384c -r 7e8f4df04d5d etc/options
--- a/etc/options	Sat Dec 19 23:19:10 2015 +0100
+++ b/etc/options	Sat Dec 19 23:25:23 2015 +0100
@@ -125,7 +125,7 @@
 public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
-public option editor_prune_delay : real = 60.0
+public option editor_prune_delay : real = 30.0
   -- "delay to prune history (delete old versions)"
 
 public option editor_update_delay : real = 0.5