changeset 62115 | 57895801cb57 |
parent 61873 | 7e8f4df04d5d |
child 62409 | e391528eff3b |
--- 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