coverity-plugin github team

[jbr...@synopsys.com]

Hi,

 

I would like to add another team to the coverity-plugin. I was added as an admin to the github repo (https://github.com/jenkinsci/coverity-plugin/settings/collaboration) but not to the coverity-plugin Developers team so I don’t have access to change the team or add a team.

 

I’d like to add the team “blackduck-detect-plugin” to the coverity-plugin (or add all members of that plugin team to the coverity-plugin Developers team).

 

Thanks,

Joel

[Daniel Beck]

> On 2. Mar 2018, at 21:40, jbr...@synopsys.com wrote:
>
> I’d like to add the team “blackduck-detect-plugin” to the coverity-plugin (or add all members of that plugin team to the coverity-plugin Developers team).

The former wouldn't be a great idea, since it's likely we'd just remove it. Teams assigned to different repos than what their name says is a well-known historical problem with how GitHub did permissions a few years ago, and I clean it up whenever I see.

Alternatively, if your group/team maintains both repos, we can create a new custom team on GitHub that's manually managed (and make you team maintainer), rather than bot-controlled.

> I would like to add another team to the coverity-plugin. I was added as an admin to the github repo (https://github.com/jenkinsci/coverity-plugin/settings/collaboration) but not to the coverity-plugin Developers team so I don’t have access to change the team or add a team.

As repo admin, you can also just add the developers as 'external collaborators' to the repo. We're probably soon switching to that anyway[1].

1: https://groups.google.com/forum/#!msg/jenkinsci-dev/EsjDADiHmtw/KSDeOsAoAQAJ

[jbr...@synopsys.com]

Thanks for the information. I've added external collaborators which will be sufficient.

As a side note the 'coverity-plugin Developers' team is just one person who is no longer a maintainer, if it's easy to clean that up that would be good.

Thanks

[jbr...@synopsys.com]

On Friday, March 2, 2018 at 3:00:39 PM UTC-7, Daniel Beck wrote:

For the existing group (from what I can tell) the only remaining member is not an active maintainer. If it's easy for you to clean that up that would be nice (not sure if it is bot-controlled... maybe it's out of sync with the repository-permissions-updater), although sounds like long-term it may not matter.

I can go ahead and add the new developers as external collaborators.

[Daniel Beck]

> On 2. Mar 2018, at 23:41, jbr...@synopsys.com wrote:
>
> For the existing group (from what I can tell) the only remaining member is not an active maintainer. If it's easy for you to clean that up that would be nice (not sure if it is bot-controlled... maybe it's out of sync with the repository-permissions-updater), although sounds like long-term it may not matter.

Bot controlled ≠ identical to upload permissions; since user names are different and we cannot reliably map between them, this is necessarily the case. It allows us to differentiate between owners and other developers (although admittedly we haven't been super consistent there).

Given the user you want removed, could you file a PR to clean up https://github.com/jenkins-infra/repository-permissions-updater/blob/master/permissions/plugin-coverity.yml as appropriate first? AFAICT the same user is still allowed to release. Just mention in your PR you want them removed from the team as well.