Git

Here is a failure that will cost you an afternoon if you have not seen it before. You open a pull request. Every required status check goes green. There are no unresolved review threads. The GitHub UI says the branch has no conflicts. You click merge, and: X Pull request ... is not mergeable: the base branch policy prohibits the merge. No indication of which policy. No indication of which rule. You push another commit, wait for CI again, try again, and get the identical message. Meanwhile other pull requests in the same repository merge without complaint, so it looks like something specific to this branch, or like GitHub is having a bad day. ...