build failure

Stream: new members

[Mark Gerads]

It says

Changes approved

and Mathlib is being rebuilt again. Does this mean I don't need to do anything?

[Eric Wieser]

If bors says it's retrying, then you don't need to do anything

[Eric Wieser]

Although it's good practice to look at the logs to guess whether it's your fault

[Bryan Gin-ge Chen]

You pushed a new commit just now, so your PR was taken out of the queue. I've "delegated" the PR to you with bors d+, so you can put it back on the queue whenever you want.

[Mark Gerads]

I'll see what that means I need to do after it shows Mathlib as successfully built.

[Bryan Gin-ge Chen]

(All you need to do is put bors r+ on its own line in a GitHub comment.)

[Eric Wieser]

Note that bors failing doesn't even mean a conflict has appeared in master - it just means that when you combine the pile of PRs into a single build on top of master, they either conflict with each other or with master

[Mark Gerads]

Is it okay for me to merge it now then? I figure I should wait; 'tis more proper. I am excited to see this contribution in Mathlib.

[Bryan Gin-ge Chen]

Sure, I think it's safe enough! It'll join the other PRs in queue: https://app.bors.tech/repositories/24316