--- 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