less frequent consolidation: it requires a full Document.update and Document.start_execution;
authorwenzelm
Sat Jun 02 19:52:16 2018 +0200 (14 months ago)
changeset 6835238272f9481c2
parent 68351 bcdc4c21ab1d
child 68353 29cbe9e8ecde
less frequent consolidation: it requires a full Document.update and Document.start_execution;
etc/options
     1.1 --- a/etc/options	Fri Jun 01 22:01:43 2018 +0200
     1.2 +++ b/etc/options	Sat Jun 02 19:52:16 2018 +0200
     1.3 @@ -156,7 +156,7 @@
     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 +public option editor_consolidate_delay : real = 2.5
     1.9    -- "delay to consolidate status of command evaluation (execution forks)"
    1.10  
    1.11  public option editor_prune_delay : real = 15