Hi Mark, On 3/7/22 15:42, Mark Wielaard wrote: > Hi Arthur, > > On Mon, 2022-03-07 at 15:32 +0100, Arthur Cohen wrote: >> I suspect this might be due to bors, our merging bot on github, and me >> asking it to merge multiple pull requests this morning (around 4 or 5). >> Not really sure. >> >> But the bug is fixed and properly placed in the history :) > > Aha, I see, you are right. For some reason bors adds commits on top of > old commits with a merge instead of doing a simple rebase on top of the > latest commit. Making the git history look like a Christmas tree: > https://code.wildebeest.org/git/mirror/gccrs/log/ > > Your new commits were indeed on top of a 5 day old commit, so the > buildbot dutifully tested it in context. And that context didn't > include the fix yet. > > Would it make sense to tell bors to do a rebase instead of a merge > before pushing to trunk? > > Cheers, > > Mark I've checked, and I don't think that bors is able to do that. Since it maintains a staging queue containing multiple PRs and then merges it onto the main branch if all tests pass, I think the christmas tree is unavoidable. I'd be happy to be proved wrong however. Kindly, Arthur