equal
deleted
inserted
replaced
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 |