etc/options
changeset 68221 dbef88c2b6c5
parent 68197 7857817403e4
child 68352 38272f9481c2
--- a/etc/options	Sat May 19 16:13:39 2018 +0200
+++ b/etc/options	Sat May 19 20:05:13 2018 +0200
@@ -250,11 +250,24 @@
   -- "maximum number of messages to keep SSH server connection alive"
 
 
-section "Theory export"
+section "Theory Export"
 
 option export_theory : bool = false
 
 
+section "Build Database"
+
+option build_database_server : bool = false
+option build_database_user : string = ""
+option build_database_password : string = ""
+option build_database_name : string = ""
+option build_database_host : string = ""
+option build_database_port : int = 0
+option build_database_ssh_host : string = ""
+option build_database_ssh_user : string = ""
+option build_database_ssh_port : int = 0
+
+
 section "Build Log Database"
 
 option build_log_database_user : string = ""