Gaëtan Gilbert (Jan 28 2021 at 14:41): Gaëtan Gilbert (Jan 28 2021 at 14:41):(https://github.com/coq/coq/pull/13796)
should we remove the codeowners file when branching?
Enrico Tassi (Jan 28 2021 at 14:47):I clearly made the 2 mistakes:
Enrico Tassi (Jan 28 2021 at 14:47):I did it more than once, so what you propose seems a good failsafe
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
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 ;-) )
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.
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 13 2024 at 01:02 UTC