We can add an || true in the end so that github doesn't show the workflow as failed.

We can add an || true in the end so that github doesn't show the workflow as failed.

@FFY00: Yeah, exactly. I just came up with the same idea :-) It would look better than "Some checks were not successful". Can you propose a PR to fix it?

Yes, I will do it in a bit. I'll ping you after to rebase this on top of it.

By the way, usually I wrote ||: rather than || true. It's an old habit. It's a bash builtin function. I don't know if it's portable. || true sounds more portable :-)

From what I gathered I think both : and true are bash builtins. But true is also a POSIX binary (see /usr/bin/true). || true is also more descriptive and doesn't require people to google what : is supposed to do :D

There's also https://help.github.com/en/actions/reference/workflow-syntax-for-github-actions#jobsjob_idstepscontinue-on-error

PR rebased on top of commit 6a78589 (GH-20097).

12 seconds, looks good 👌

Good: "Tests / Check for source changes (pull_request)" is no longer marked as failed, but "build" jobs continue to be skipped! Sadly, the reason for the skip is not mentioned :-( But it's ok, it's not a big deal. Most people are likely to not bother with it :-)
https://help.github.com/en/actions/reference/workflow-syntax-for-github-actions#jobsjob_idif

Yes, it would be good to be able to provide a reason but I don't really think it's that big of a deal :P As long as the devs are aware of this it should be perfectly fine.

Ok, great! I confirm that I get a green merge button: I could merge the PR, even with skipped build jobs. Thanks again @FFY00 for fixing our CI config ;-)

I now close the issue since it proved that it works. (It doesn't prevent to merge a doc-only PR.)