diff -r c97abf0fa0c1 -r 7e6ecd04b5fe etc/options
--- 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"