etc/options
changeset 65595 ffd8283b7be0
parent 65456 31e8a86971a8
child 65782 4935bac8a850
     1.1 --- a/etc/options	Thu Apr 27 15:56:55 2017 +0200
     1.2 +++ b/etc/options	Thu Apr 27 16:54:45 2017 +0200
     1.3 @@ -232,3 +232,15 @@
     1.4  
     1.5  option ssh_alive_interval : real = 30
     1.6    -- "time interval to keep SSH server connection alive (seconds)"
     1.7 +
     1.8 +
     1.9 +section "Build Log Database"
    1.10 +
    1.11 +option build_log_database_user : string = ""
    1.12 +option build_log_database_password : string = ""
    1.13 +option build_log_database_name : string = ""
    1.14 +option build_log_database_host : string = ""
    1.15 +option build_log_database_port : int = 0
    1.16 +option build_log_ssh_host : string = ""
    1.17 +option build_log_ssh_user : string = ""
    1.18 +option build_log_ssh_port : int = 0