summaryrefslogtreecommitdiff
path: root/baserock_gerrit
diff options
context:
space:
mode:
authorSam Thursfield <sam.thursfield@codethink.co.uk>2015-08-24 11:56:04 +0100
committerSam Thursfield <sam.thursfield@codethink.co.uk>2015-08-24 11:57:16 +0100
commitcddaccd2ac9d5b34a693af5532de293690ad409c (patch)
tree747684ca7e5fad1d9fe37bf0236a342a4e1999da /baserock_gerrit
parent9bf0c1b5bc0de8ccf3519e3c3d9758a1f1fcb504 (diff)
downloadinfrastructure-cddaccd2ac9d5b34a693af5532de293690ad409c.tar.gz
baserock_gerrit: Allow Mergers group to force push (except to 'master')
Anyone who can create branches really needs to be able to delete them as well. Change-Id: Id1c315262545dd5ba18c1fd257dcf8a18d903374
Diffstat (limited to 'baserock_gerrit')
-rw-r--r--baserock_gerrit/All-Projects/project.config10
1 files changed, 6 insertions, 4 deletions
diff --git a/baserock_gerrit/All-Projects/project.config b/baserock_gerrit/All-Projects/project.config
index e418ac0b..f3069904 100644
--- a/baserock_gerrit/All-Projects/project.config
+++ b/baserock_gerrit/All-Projects/project.config
@@ -61,7 +61,7 @@
push = group Project Owners
create = group Mergers
forgeAuthor = group Mergers
- push = group Mergers
+ push = +force group Mergers
create = group Mirroring Tools
forgeAuthor = group Mirroring Tools
@@ -69,11 +69,13 @@
push = +force group Mirroring Tools
-# We allow Lorry to force-push to personal branches, but don't ever let
-# it force-push to master as this may undo merges that Gerrit just did
-# and really confuse things.
+# Nobody should be able to force push to 'master'. In particular, if Lorry
+# can force-push master then it will do, in the course of mirroring from
+# git.baserock.org, and this may undo merges that Gerrit just did and really
+# confuse things.
[access "refs/heads/master"]
exclusiveGroupPermissions = push
+ push = block +force group Mergers
push = block +force group Mirroring Tools