# HG changeset patch # User Fabian Huch # Date 1738445409 -3600 # Node ID e7acf8c4572e0d3e7b18fbb1611c1df8a8d012ef # Parent 0dc7b3253aaaafd9a3261056d2490da65d82688c clarified option name; diff -r 0dc7b3253aaa -r e7acf8c4572e etc/options --- 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 diff -r 0dc7b3253aaa -r e7acf8c4572e src/Pure/Build/build_manager.scala --- 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,