Race condition when PR gets pushed while bors dequeues?

Have a look at [this](https://github.com/rust-lang/miri/pull/3128#issuecomment-1769194140):
> Commit https://github.com/rust-lang/miri/commit/e9cab75506a68a5bfc102ce734f357d3f1c36dc2 has been approved by RalfJung
> Testing commit https://github.com/rust-lang/miri/commit/dfd436936396ff080d1b4b09ae1adcf658a44f20 with merge https://github.com/rust-lang/miri/commit/424768dae2adc28b0447d1929916423b68eaad77...

I approved one commit but then it tests a different commit! Surely that should never ever happen, landing unapproved changes?

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Race condition when PR gets pushed while bors dequeues? #198

RalfJung
openedon Oct 18, 2023

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Race condition when PR gets pushed while bors dequeues? #198

Description

RalfJungopenedon Oct 18, 2023

Metadata