changeset 70778 | f326596f5752 |
parent 70777 | b52a12559d92 |
child 70787 | 15656ad28691 |
--- a/etc/options Tue Oct 01 19:08:24 2019 +0200 +++ b/etc/options Tue Oct 01 19:54:42 2019 +0200 @@ -162,7 +162,7 @@ public option editor_output_delay : real = 0.1 -- "delay for prover output (markup, common messages etc.)" -public option editor_consolidate_delay : real = 2.0 +public option editor_consolidate_delay : real = 3.0 -- "delay to consolidate status of command evaluation (execution forks)" public option editor_prune_delay : real = 15