On 4/3/2020 2:32 PM, Victor Stinner wrote:
tl; dr Maybe the 1090 pending pull requests will have to be rebased on master to be able to be merged, unless we enhance our CI to always test PRs after rebasing them on the master branch.
I hope you mean doing an update merge rather than a rebase.
I am otherwise not sure what you are saying. Sometimes when I request an up-to-date webpage for a PR, it has a notice that there is a merge conflict and that the PR cannot be merged even though all tests, when last run, were green. The tests do not have to be rerun for this to happen.
The latest occurrence was for a PR that modified a blurb file that was deleted after the blurb was moved to the master log for 3.9.0a5. (This was not nice to fix, so I will avoid in the future by not commit such edits until otherwise reade to merge.) So my impression is that github tries to merge the PR into master on every page request.
I very much appreciate the work being done to prevent spurious CI failures.