changeset 66379 | 6392766f3c25 |
parent 66160 | 33f759742887 |
child 66780 | bf54ca580bf2 |
--- a/etc/options Tue Aug 08 12:21:29 2017 +0200 +++ b/etc/options Tue Aug 08 22:13:05 2017 +0200 @@ -155,6 +155,9 @@ public option editor_output_delay : real = 0.1 -- "delay for prover output (markup, common messages etc.)" +public option editor_consolidate_delay : real = 1.0 + -- "delay to consolidate status of command evaluation (execution forks)" + public option editor_prune_delay : real = 15 -- "delay to prune history (delete old versions)"