| changeset 65264 | 7e6ecd04b5fe |
| parent 65141 | c706b57b1694 |
| child 65448 | 9bc3b57c1fa7 |
--- a/etc/options Wed Mar 15 15:39:15 2017 +0100 +++ b/etc/options Wed Mar 15 15:50:28 2017 +0100 @@ -153,6 +153,9 @@ public option editor_prune_delay : real = 15 -- "delay to prune history (delete old versions)" +option editor_prune_size : int = 0 + -- "retained size of pruned history (delete old versions)" + public option editor_update_delay : real = 0.5 -- "delay for physical GUI updates"