On Oct 4, 2020, at 15:55, Terry Reedy <[email protected]> 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
  [email protected] -- []
_______________________________________________
Python-Dev mailing list -- [email protected]
To unsubscribe send an email to [email protected]
https://mail.python.org/mailman3/lists/python-dev.python.org/
Message archived at 
https://mail.python.org/archives/list/[email protected]/message/XQYAE2ZQVTAK7PIER6HXSZXEAFW2TJ3K/
Code of Conduct: http://python.org/psf/codeofconduct/

Reply via email to