changeset 76474 | 287c3adcdcd6 |
parent 76471 | 1f0b2d7298d9 |
child 76578 | 06b001094ddb |
--- a/etc/options Sun Nov 06 19:25:48 2022 +0100 +++ b/etc/options Sun Nov 06 20:27:35 2022 +0100 @@ -193,7 +193,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 = 1.0 -- "delay to consolidate status of command evaluation (execution forks)" public option editor_prune_delay : real = 15