etc/options
changeset 80252 96543177ab7e
parent 80246 245dd5f82462
child 80253 a3c2868cfb5d
equal deleted inserted replaced
80251:6ae378791c52 80252:96543177ab7e
   465 
   465 
   466 option build_manager_ssh_host : string = "build.proof.cit.tum.de" for connection
   466 option build_manager_ssh_host : string = "build.proof.cit.tum.de" for connection
   467   -- "ssh server on which build manager runs"
   467   -- "ssh server on which build manager runs"
   468 option build_manager_ssh_user : string = "" for connection
   468 option build_manager_ssh_user : string = "" for connection
   469   -- "ssh user to access build manager system"
   469   -- "ssh user to access build manager system"
       
   470 
       
   471 option build_manager_ssh_group : string = "isabelle"
       
   472   -- "common group for users on build manager system"
       
   473 
   470 option build_manager_ssh_port : int = 0 for connection
   474 option build_manager_ssh_port : int = 0 for connection
   471 
   475 
   472 
   476 
   473 section "Build Manager Database"
   477 section "Build Manager Database"
   474 
   478