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 -- Gcc-rust mailing list Gcc-rust@gcc.gnu.org https://gcc.gnu.org/mailman/listinfo/gcc-rust
