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