Merge branch 'jc/ci-skip-same-commit' into maint-2.42

Tweak GitHub Actions CI so that pushing the same commit to multiple branch tips at the same time will not waste building and testing the same thing twice. * jc/ci-skip-same-commit: ci: avoid building from the same commit in parallel