etc/options
changeset 65595 ffd8283b7be0
parent 65456 31e8a86971a8
child 65782 4935bac8a850
--- a/etc/options	Thu Apr 27 15:56:55 2017 +0200
+++ b/etc/options	Thu Apr 27 16:54:45 2017 +0200
@@ -232,3 +232,15 @@
 
 option ssh_alive_interval : real = 30
   -- "time interval to keep SSH server connection alive (seconds)"
+
+
+section "Build Log Database"
+
+option build_log_database_user : string = ""
+option build_log_database_password : string = ""
+option build_log_database_name : string = ""
+option build_log_database_host : string = ""
+option build_log_database_port : int = 0
+option build_log_ssh_host : string = ""
+option build_log_ssh_user : string = ""
+option build_log_ssh_port : int = 0