| changeset 80253 | a3c2868cfb5d |
| parent 80252 | 96543177ab7e |
| child 80281 | 17d2f775907a |
--- a/etc/options Wed Jun 05 15:01:20 2024 +0200 +++ b/etc/options Wed Jun 05 15:01:31 2024 +0200 @@ -465,6 +465,7 @@ option build_manager_ssh_host : string = "build.proof.cit.tum.de" for connection -- "ssh server on which build manager runs" + option build_manager_ssh_user : string = "" for connection -- "ssh user to access build manager system"