reopen !4#1287

Stream: mathlib4

[Matthew Ballard]

bors closed this pr after merging a different pr from the branch it was pointing at. Would someone with permissions be able to reopen it? I @maintainers Thanks.

[Eric Wieser]

There's a bors setting we can turn on to disable this

[Reid Barton]

It looks like the PR was opened into the slice branch. So it needs to be opened as a PR into master anyways.

[Eric Wieser]

(it's already turned on in mathlib3)

[Eric Wieser]

Reid, the setting has bors automatically switch the target branch

[Matthew Ballard]

Yes. I had a different mental model for a dependent pr here.

[Matthew Ballard]

I also assumed (without any reason) that this setting existed and was enabled.

[Matthew Ballard]

My apologies.

[Eric Wieser]

@Matthew Ballard, you can reopen the PR yourself if you push a new slice branch`

[Matthew Ballard]

I’ll try

[Eric Wieser]

Oh, I found a button to do so online

[Eric Wieser]

It's open again

[Eric Wieser]

You still need to change the target to master, and probably merge master

[Eric Wieser]

Can you make a PR to copy across the bors setting from mathlib3?

[Matthew Ballard]

Eric Wieser said:

Oh, I found a button to do so online

Yes. It was grayed out for me.

[Matthew Ballard]

Thanks!

[Eric Wieser]

The button I'm talking about was the "undelete the slice branch" button, which I had to go to the closed PR to see. The "reopen PR button" was also grayed out for me until I did that.

[Matthew Ballard]

Huh. I thought I clicked that and the reopen button was still grayed out. Whatever I did, thanks again.

[Eric Wieser]

The summary is that I think you don't need maintainer powers to undo that type of mess, but it's not easy to work out how to do it either.

Either way, thanks for the bors PR; now this shouldn't happen again.