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/76F6AF4F-817A-4877-A1FF-20D01929254C%40dwheeler.com.
