--- a/etc/options Sat Feb 01 22:28:32 2025 +0100
+++ b/etc/options Sat Feb 01 22:30:09 2025 +0100
@@ -490,7 +490,7 @@
option build_manager_ssh_user : string = "" for connection
-- "ssh user to access build manager system"
-option build_manager_ssh_group : string = "isabelle"
+option build_manager_group : string = "isabelle"
-- "common group for users on build manager system"
option build_manager_ssh_port : int = 0 for connection
--- a/src/Pure/Build/build_manager.scala Sat Feb 01 22:28:32 2025 +0100
+++ b/src/Pure/Build/build_manager.scala Sat Feb 01 22:30:09 2025 +0100
@@ -1635,7 +1635,7 @@
def init_dirs(): Unit =
List(pending, finished).foreach(dir => sync_permissions(Isabelle_System.make_directory(dir)))
- val ssh_group: String = options.string("build_manager_ssh_group")
+ val ssh_group: String = options.string("build_manager_group")
def open_cluster_ssh(): SSH.Session =
SSH.open_session(options,