Closed RalfJung closed 4 years ago
bors r+
Thanks!
I had a typo in there and you were too fast.^^ Sorry for that.
Yeah, my approach to merging most PRs is basically r+ immediately, because
^^
bors merge
bors r+
Thanks!