Zulip Chat Archive

Stream: general

Topic: bors ate my PR?

Andrew Yang (Aug 17 2022 at 04:47):

When bors merged #15809, it somehow managed to revert the changes in another PR of mine (#15806) that was in the same batch.
Should I reopen the eaten PR? Or would bors get confused and I should open a new PR?

Johan Commelin (Aug 17 2022 at 05:30):

Very weird. I think I would just open a new PR.

Junyan Xu (Aug 17 2022 at 05:33):

I see you have two revert commits in #15809 and that's probably why bors gets confused (especially since #15086 shares the first two commits with #15809). Since the squashed commits in mathlib doesn't overlap with commits in #15086, reopening is probably OK, but just to be safe ...

Andrew Yang (Aug 17 2022 at 05:41):

I open a new PR at #16094 in case bors gets confused again.

Johan Commelin (Aug 17 2022 at 05:44):

Gave you a bors d+

Last updated: Dec 20 2023 at 11:08 UTC