Stream: Coq devs & plugin devs

Topic: review request spam on backport PR


view this post on Zulip Gaëtan Gilbert (Jan 28 2021 at 14:41):

(https://github.com/coq/coq/pull/13796)
should we remove the codeowners file when branching?

view this post on Zulip Enrico Tassi (Jan 28 2021 at 14:47):

I clearly made the 2 mistakes:

view this post on Zulip Enrico Tassi (Jan 28 2021 at 14:47):

I did it more than once, so what you propose seems a good failsafe

view this post on Zulip Enrico Tassi (Jan 28 2021 at 14:48):

@Théo Zimmermann suggests to never close the branch used for backports, which would avoid this, but I don't like the git mumbo-jumbo you have to do

view this post on Zulip Enrico Tassi (Jan 28 2021 at 14:48):

So I don't really know if removing codeowners is a good idea in general (for sure it is if I'm the RM ;-) )

view this post on Zulip Théo Zimmermann (Jan 28 2021 at 14:51):

Before the advent of draft PR, we did indeed remove the CODEOWNERS file from release branches.

view this post on Zulip Théo Zimmermann (Jan 28 2021 at 14:52):

We could make it a systematic step of the release process (by adding it to the documented release checkboxes).


Last updated: Oct 21 2021 at 21:03 UTC