Asking here first instead of filing a bug, because I’m not sure if this is a bug or just a misunderstanding.
A colleague commented
bors r+ on a branch this afternoon, then realised it shouldn’t be merged yet and commented
bors r- right after. This correctly aborted the batch that had started, but then the PR was included in the next batch and merged, which is not what I would have expected: