diff -r e7acf8c4572e -r d064d6f36ce1 etc/options
--- a/etc/options	Sat Feb 01 22:30:09 2025 +0100
+++ b/etc/options	Sat Feb 01 22:31:19 2025 +0100
@@ -240,6 +240,9 @@
 
 section "Build Manager"
 
+option build_manager_group : string = "isabelle"
+  -- "common group for users on build manager system"
+
 option build_manager_dir : string = "/srv/build"
   -- "directory for submissions on build server"
 
@@ -485,16 +488,10 @@
 section "Build Manager SSH"
 
 option build_manager_ssh_host : string = "build.proof.cit.tum.de" for connection
-  -- "ssh server on which build manager runs"
-
+option build_manager_ssh_port : int = 0 for connection
 option build_manager_ssh_user : string = "" for connection
   -- "ssh user to access build manager system"
 
-option build_manager_group : string = "isabelle"
-  -- "common group for users on build manager system"
-
-option build_manager_ssh_port : int = 0 for connection
-
 option build_manager_cluster_ssh_host : string = "localhost" for connection
 option build_manager_cluster_ssh_user : string = "" for connection
 option build_manager_cluster_ssh_port : int = 0 for connection