Ned Deily schrieb am 05.10.20 um 01:19:
On Oct 4, 2020, at 15:55, Terry Reedy 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.
Thank you Ned, and good to know. Stefan