Bors batch disappeared

Stream: general

[Riccardo Brasca]

Something happened to a previous bors batch, it somehow disappeared. I don't know its number, but I had #9813 in it (I noticed it was a big batch), that wasn't merged but it's not waiting to run anymore.

[Sebastien Gouezel]

bors has crached on a 17PR batch. I have just revalidated all of them.

[Yaël Dillies]

17?!? :scream:

[Eric Wieser]

Well now there are 21 in the batch

[Sebastien Gouezel]

(see https://app.bors.tech/repositories/24316/log). Could we have #bors for this?

[Sebastien Gouezel]

It already works!

[Sebastien Gouezel]

You guys are just awesome :-)

[Eric Wieser]

(that link only works for maintainers)

[Yaël Dillies]

#bors works for me

[Eric Wieser]

But the/log one doesn't, right?

[Yaël Dillies]

Nope, that doesn't :sad:

[Yaël Dillies]

Time for me to become a maintainer, I guess :rofl:

[Eric Wieser]

Looks like the monster batch got split in two by conflicts

[Yaël Dillies]

Yup, I was about to say that my PR #9899 is going to conflict quite a lot with all the other ones.

[Yaël Dillies]

I'd advise they all merge master.

[Eric Wieser]

It'll become obvious once bors gets through the first batch, I'd hope

[Yaël Dillies]

Sure. If I'm right, it shouldn't take too long to fail anyway.

[Floris van Doorn]

Yaël Dillies said:

Yup, I was about to say that my PR #9899 is going to conflict quite a lot with all the other ones.

Git is pretty good at merging, even when you rename a file and someone else makes changes to that file. I don't think your PR is likely to cause many conflicts.

[Floris van Doorn]

(but there are some very quick failures by bors, which is probably a merge conflict, so maybe I'm wrong)