changeset 57867 | abae8aff6262 |
parent 56875 | f6259d6fb565 |
child 57974 | ba0b6c2338f0 |
--- a/etc/options Tue Aug 05 19:58:07 2014 +0200 +++ b/etc/options Tue Aug 05 20:40:35 2014 +0200 @@ -117,6 +117,9 @@ public option editor_output_delay : real = 0.1 -- "delay for prover output (markup, common messages etc.)" +public option editor_prune_delay : real = 60.0 + -- "delay to prune history (delete old versions)" + public option editor_update_delay : real = 0.5 -- "delay for physical GUI updates"