author | Fabian Huch <huch@in.tum.de> |
Wed, 05 Jun 2024 15:01:31 +0200 | |
changeset 80253 | a3c2868cfb5d |
parent 80252 | 96543177ab7e |
child 80254 | 6b3374d208b8 |
etc/options | file | annotate | diff | comparison | revisions |
--- 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"