out-of-date pull request

Stream: mathlib4

[Iván Renison]

Hello, my pull request is out-of-date with the base branch but doesn't have merge conflicts, and is in awaiting-review, should I merge the changes of the base branch to my branch?

[Eric Wieser]

There's no need to unless there are merge conflicts, which there do not appear to be

[Iván Renison]

Ok, thanks

[Iván Renison]

How much time it's expected that I will have to wait until the pull request is reviewed?

[Eric Rodriguez]

We're currently in a bit of a crossroads because there's issues with the infrastructure caused by one of them just disappearing support-wise overnight

[Mario Carneiro]

that doesn't impact the review though

[Eric Rodriguez]

PR reviewing is very time consuming though even in normal times so I'd personally sit back and try not to stress about it

[Eric Rodriguez]

Mario Carneiro said:

that doesn't impact the review though

Are we still reviewing stuff? How are we merging?

[Mario Carneiro]

we aren't merging, but we are still reviewing

[Mario Carneiro]

some people are putting things like "bors r+" even though bors isn't listening, to register approval

[Johan Commelin]

maintainer merge still works. I've been using that to create a log of mergeable PRs

[Eric Wieser]

I think the reason this question came up is that github is showing this new button after we reconfigured some settings:

image.png

[Jireh Loreaux]

bors r+ works insofar as the PR gets a "ready to merge" label though, right? Because that's just the GitHub bot.