Merged by bors merged by bors

Stream: general

[Yaël Dillies]

Wow, #10999 was really merged by bors!

[Thomas Browning]

Happed to mine too: #10937

[Kevin Buzzard]

Will I wake up tomorrow to [Merged by Bors] - [Merged by Bors] - [Merged by Bors] - [Merged by Bors] - [Merged by Bors] - [Merged by Bors] - [Merged by Bors] - [Merged by Bors] - ...?

[Eric Rodriguez]

Thomas's commits also seem to be in a weird github state - at the bottom it says the commits are unmerged