etc/options

--- a/etc/options	Tue Aug 08 12:21:29 2017 +0200
+++ b/etc/options	Tue Aug 08 22:13:05 2017 +0200
@@ -155,6 +155,9 @@
 public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
+public option editor_consolidate_delay : real = 1.0
+  -- "delay to consolidate status of command evaluation (execution forks)"
+
 public option editor_prune_delay : real = 15
   -- "delay to prune history (delete old versions)"