Stream: new members
Topic: build failure
Mark Gerads (Mar 01 2021 at 20:17):
and Mathlib is being rebuilt again. Does this mean I don't need to do anything?
Eric Wieser (Mar 01 2021 at 20:18):
If bors says it's retrying, then you don't need to do anything
Eric Wieser (Mar 01 2021 at 20:19):
Although it's good practice to look at the logs to guess whether it's your fault
Bryan Gin-ge Chen (Mar 01 2021 at 20:19):
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 (Mar 01 2021 at 20:21):
I'll see what that means I need to do after it shows Mathlib as successfully built.
Bryan Gin-ge Chen (Mar 01 2021 at 20:23):
(All you need to do is put
bors r+ on its own line in a GitHub comment.)
Eric Wieser (Mar 01 2021 at 20:25):
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 (Mar 01 2021 at 20:30):
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 (Mar 01 2021 at 20:35):
Sure, I think it's safe enough! It'll join the other PRs in queue: https://app.bors.tech/repositories/24316
Last updated: May 11 2021 at 12:15 UTC