On Oct 4, 2020, at 15:55, Terry Reedy <tjre...@udel.edu> wrote: > > On 10/4/2020 2:32 PM, Mariatta wrote: >> This is a known issue and I have brought it up in GitHub OS Maintainers >> Feedback Group. It happens to other projects as well. >> Currently we have branch protection rule where even administrators couldnt >> merge the PR unless all the required checks passed. >> Perhaps we can relax the rule to allow administrators to merge the stuck >> PRs. At least temporarily until Travis/GitHub fixes it. Does this sound okay? > > If we are told how to ping the admins, it would be better than being stuck.
If you run into a problem like this with a stuck PR, contact the release manager for the branch directly via email. Release managers can override the restrictions and we don't always read every list immediately. Because this was a trivial change and because of time zones, I've taken the liberty of acting in Pablo's behalf: it's now merged. -- Ned Deily n...@python.org -- [] _______________________________________________ Python-Dev mailing list -- python-dev@python.org To unsubscribe send an email to python-dev-le...@python.org https://mail.python.org/mailman3/lists/python-dev.python.org/ Message archived at https://mail.python.org/archives/list/python-dev@python.org/message/XQYAE2ZQVTAK7PIER6HXSZXEAFW2TJ3K/ Code of Conduct: http://python.org/psf/codeofconduct/
