etc/options
changeset 65264 7e6ecd04b5fe
parent 65141 c706b57b1694
child 65448 9bc3b57c1fa7
     1.1 --- a/etc/options	Wed Mar 15 15:39:15 2017 +0100
     1.2 +++ b/etc/options	Wed Mar 15 15:50:28 2017 +0100
     1.3 @@ -153,6 +153,9 @@
     1.4  public option editor_prune_delay : real = 15
     1.5    -- "delay to prune history (delete old versions)"
     1.6  
     1.7 +option editor_prune_size : int = 0
     1.8 +  -- "retained size of pruned 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