Sounds good to me. I think requiring a pull request is uncontroversial. Requiring the tests to pass can sometimes seem like there should be exceptions when the tests fail for reasons which are perceived to not relate to the code being merged, but (1) fortunately our checks have been mostly quite reliable as far as I've noticed on this project, and (2) merging without passing checks can easily lead to situations where checks are failing on develop (and new branches) and that is just unnecessary trouble for pretty much everyone including the person who thought they were saving time by bypassing them.
On August 24, 2022 8:17:31 AM PDT, "David A. Wheeler" <[email protected]> wrote: >I propose enabling "branch protection" on our set.mm GitHub repo, branch >"develop". > >Specifically I propose enabling branch protection with these rules: >* Require a pull request before merging. When enabled, all commits must be >made to a non-protected branch and submitted via a pull request before they >can be merged into a branch that matches this rule. >* Require status checks to pass before merging. [We] Choose which status >checks must pass before branches can be merged into a branch that matches this >rule. When enabled, commits must first be pushed to another branch, then >merged or pushed directly to a branch that matches this rule after status >checks have passed. > >This change will mechanically enforce what we're already doing. GitHub will >then ensure that every proposed change must be posted as a branch, where >people & tools can review before it's accepted. > >Rationale: This will help prevent accidentally accepting a change that isn't >ready. Mistakes happen, and this will make it less likely that mistakes mess >up anything. Enabling branch protection is a widely-applied best practice. > >We could also, in the future, mechanically enforce "must be approved by >someone else before accepting" if we wanted to. But that's not what I'm >proposing at this time. > >--- David A. Wheeler > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/F2FBADC7-555C-4E3C-ADC2-AB473E0408D7%40panix.com.
