diff options
| -rwxr-xr-x | update_jdn.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/update_jdn.sh b/update_jdn.sh index b1d4a246..6e965caa 100755 --- a/update_jdn.sh +++ b/update_jdn.sh @@ -72,6 +72,7 @@ user_host_groups['helmut','*']="$sudo_groups" user_host_groups['holger','*']="$sudo_groups" user_host_groups['holger','jenkins']="reproducible,${user_host_groups['holger','*']}" user_host_groups['mattia','*']="$sudo_groups" +user_host_groups['mattia','jenkins']="reproducible,${user_host_groups['mattia','*']}" user_host_groups['phil','jenkins-test-vm']="$sudo_groups,libvirt,libvirt-qemu" user_host_groups['phil','profitbricks-build10-amd64']="$sudo_groups" user_host_groups['phil','jenkins']='' |