GitHub "Beman Leads" label is up!

Hello,

I configured the GitHub org to propagate Beman Leads label in all repos (as stated in beman/docs/BEMAN_STANDARD.md at main · bemanproject/beman · GitHub).

Notes:

  • It works by design for new repos!
    Here is a PoC
  • I had to manually add labels for existing repos…

TLDR: It should work now for all repos in the Beman org!
Members please use @leads (Beman Leads) on Discourse and @Beman Leads label on GitHub if you really need Leads input (e.g., updates in Beman Standard etc)

2 Likes

I would recommand adding a @ leads team to the GitHub org.

You can add a “team” under the org setting and name it leads, then @ leads would also work on GitHub iirc. We can simplify codeowner file if this is added.

See: Sign in to GitHub · GitHub
Creating a team - GitHub Docs

Good idea. I just did this.

2 Likes

Should we also add other teams?

E.g. admin
E.g. codeowners

?

I vote to keep it simple until we can’t bear the simple thing anymore. If we find the “beman leads” label isn’t helpful for “admin” or “codeowners” things, we can adjust as needed.

3 Likes