etc/options

--- a/etc/options	Tue Jun 04 18:55:55 2024 +0200
+++ b/etc/options	Wed Jun 05 15:01:20 2024 +0200
@@ -467,6 +467,10 @@
   -- "ssh server on which build manager runs"
 option build_manager_ssh_user : string = "" for connection
   -- "ssh user to access build manager system"
+
+option build_manager_ssh_group : string = "isabelle"
+  -- "common group for users on build manager system"
+
 option build_manager_ssh_port : int = 0 for connection