etc/options
changeset 65782 4935bac8a850
parent 65595 ffd8283b7be0
child 66158 ad83d4971dfe
     1.1 --- a/etc/options	Mon May 08 21:51:26 2017 +0200
     1.2 +++ b/etc/options	Mon May 08 21:58:15 2017 +0200
     1.3 @@ -244,3 +244,4 @@
     1.4  option build_log_ssh_host : string = ""
     1.5  option build_log_ssh_user : string = ""
     1.6  option build_log_ssh_port : int = 0
     1.7 +option build_log_history : int = 30  -- "length of relevant history (in days)"