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