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