# HG changeset patch # User wenzelm # Date 1527961936 -7200 # Node ID 38272f9481c2cdae98841a384863d6473694429f # Parent bcdc4c21ab1dd60e7e36ef39e720e2f4867e6696 less frequent consolidation: it requires a full Document.update and Document.start_execution; diff -r bcdc4c21ab1d -r 38272f9481c2 etc/options --- a/etc/options Fri Jun 01 22:01:43 2018 +0200 +++ b/etc/options Sat Jun 02 19:52:16 2018 +0200 @@ -156,7 +156,7 @@ public option editor_output_delay : real = 0.1 -- "delay for prover output (markup, common messages etc.)" -public option editor_consolidate_delay : real = 1.0 +public option editor_consolidate_delay : real = 2.5 -- "delay to consolidate status of command evaluation (execution forks)" public option editor_prune_delay : real = 15