prune old document versions more frequently, for reduced heap usage;
authorwenzelm
Sat Dec 19 23:25:23 2015 +0100 (2015-12-19)
changeset 618737e8f4df04d5d
parent 61872 fcb4d24c384c
child 61874 a942e237c9e8
prune old document versions more frequently, for reduced heap usage;
etc/options
     1.1 --- a/etc/options	Sat Dec 19 23:19:10 2015 +0100
     1.2 +++ b/etc/options	Sat Dec 19 23:25:23 2015 +0100
     1.3 @@ -125,7 +125,7 @@
     1.4  public option editor_output_delay : real = 0.1
     1.5    -- "delay for prover output (markup, common messages etc.)"
     1.6  
     1.7 -public option editor_prune_delay : real = 60.0
     1.8 +public option editor_prune_delay : real = 30.0
     1.9    -- "delay to prune history (delete old versions)"
    1.10  
    1.11  public option editor_update_delay : real = 0.5