# 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