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:
Hmm, bors reports build 0.0.4 so “a while”. Also I think I see what happened, the wrong PR got unreviewed, so this is probably https://github.com/bors-ng/bors-ng/issues/349 and will be fixed if I update. Sorry for the noise!
No problem. Version reporting in the Docker builds is actually kinda messed up, now that I look at it. Working on that now!
Okay, I just pushed a new Docker image to borsng/bors-ng. It should report its version properly now.