diff -r a7cf464933f7 -r 57895801cb57 etc/options
--- a/etc/options	Sat Jan 09 22:22:17 2016 +0100
+++ b/etc/options	Sun Jan 10 23:25:11 2016 +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 = 30.0
+public option editor_prune_delay : real = 15
   -- "delay to prune history (delete old versions)"
 
 public option editor_update_delay : real = 0.5