etc/options
changeset 68381 2fd3a6d6ba2e
parent 68352 38272f9481c2
child 68491 f0f83ce0badd
equal deleted inserted replaced
68380:f249e1f5623b 68381:2fd3a6d6ba2e
   154   -- "delay for machine-generated input that may outperform user edits"
   154   -- "delay for machine-generated input that may outperform user edits"
   155 
   155 
   156 public option editor_output_delay : real = 0.1
   156 public option editor_output_delay : real = 0.1
   157   -- "delay for prover output (markup, common messages etc.)"
   157   -- "delay for prover output (markup, common messages etc.)"
   158 
   158 
   159 public option editor_consolidate_delay : real = 2.5
   159 public option editor_consolidate_delay : real = 2.0
   160   -- "delay to consolidate status of command evaluation (execution forks)"
   160   -- "delay to consolidate status of command evaluation (execution forks)"
   161 
   161 
   162 public option editor_prune_delay : real = 15
   162 public option editor_prune_delay : real = 15
   163   -- "delay to prune history (delete old versions)"
   163   -- "delay to prune history (delete old versions)"
   164 
   164