diff -r 6cd11999f3a3 -r 4935bac8a850 etc/options
--- a/etc/options	Mon May 08 21:51:26 2017 +0200
+++ b/etc/options	Mon May 08 21:58:15 2017 +0200
@@ -244,3 +244,4 @@
 option build_log_ssh_host : string = ""
 option build_log_ssh_user : string = ""
 option build_log_ssh_port : int = 0
+option build_log_history : int = 30  -- "length of relevant history (in days)"