# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1717592491 -7200
# Node ID a3c2868cfb5d0c270989df98b9c347cb350f7aa3
# Parent  96543177ab7e532b9de2d025ea28737396c8b4c1
tuned;

diff -r 96543177ab7e -r a3c2868cfb5d 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"