etc/options
changeset 70778 f326596f5752
parent 70777 b52a12559d92
child 70787 15656ad28691
--- a/etc/options	Tue Oct 01 19:08:24 2019 +0200
+++ b/etc/options	Tue Oct 01 19:54:42 2019 +0200
@@ -162,7 +162,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 = 3.0
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 public option editor_prune_delay : real = 15