etc/options
changeset 68221 dbef88c2b6c5
parent 68197 7857817403e4
child 68352 38272f9481c2
     1.1 --- a/etc/options	Sat May 19 16:13:39 2018 +0200
     1.2 +++ b/etc/options	Sat May 19 20:05:13 2018 +0200
     1.3 @@ -250,11 +250,24 @@
     1.4    -- "maximum number of messages to keep SSH server connection alive"
     1.5  
     1.6  
     1.7 -section "Theory export"
     1.8 +section "Theory Export"
     1.9  
    1.10  option export_theory : bool = false
    1.11  
    1.12  
    1.13 +section "Build Database"
    1.14 +
    1.15 +option build_database_server : bool = false
    1.16 +option build_database_user : string = ""
    1.17 +option build_database_password : string = ""
    1.18 +option build_database_name : string = ""
    1.19 +option build_database_host : string = ""
    1.20 +option build_database_port : int = 0
    1.21 +option build_database_ssh_host : string = ""
    1.22 +option build_database_ssh_user : string = ""
    1.23 +option build_database_ssh_port : int = 0
    1.24 +
    1.25 +
    1.26  section "Build Log Database"
    1.27  
    1.28  option build_log_database_user : string = ""