author | wenzelm |
Sat, 19 Dec 2015 23:25:23 +0100 | |
changeset 61873 | 7e8f4df04d5d |
parent 61872 | fcb4d24c384c |
child 61874 | a942e237c9e8 |
etc/options | file | annotate | diff | comparison | revisions |
--- 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