Incompatible PR

Stream: general

[Yaël Dillies]

#8892 and #8974 are incompatible. That's why bors is failing. Is there anything to do? (and yeah sorry I knew it but overthought it)

[Yakov Pechersky]

Merge master into your pr, merge the other pr into yours, fix errors

[Bryan Gin-ge Chen]

Thanks for tracking this down! As a "reward", I've taken your PR off the queue and marked it dependent on #8974.

[Yaël Dillies]

Thanks! I knew they were incompatible and I wasn't thinking they would be sent on the queue simultaneously :grinning:

[Oliver Nash]

Thanks @Yaël Dillies !