I’ve been debugging some CI issues that came up today (after the repo lay dormant for some months so no CI ran), and I noticed something odd: the commit shown by
git show is not the same as the one in
TRAVIS_COMMIT! For some examples for this, check this or this or this.
I did not push to the PR between the job being created and the job running, so that’s not the problem. Instead there seem to be two merge commits merging the same two parent commits: This one and this one, and it uses one for
TRAVIS_COMMIT but checks out the other. Hu?
git checkout $TRAVIS_COMMIT to our build scripts and that in fact fixed (one of) the issues we had.