Improve GitHub CI Actions: remove the build of executables if only the docsite is touched

[rorleth]

Currently, every pull requests builds the executables, even if only the docsite is changed by a PR. This slows the checkin process down and it would incur additional costs if this wasn't a public repo (GitHub only gives you those actions for free if the repo is public). See ci.yml (where those are kicked off) and docsite.yml (where the Docusaurus build is being kicked off conditionally on files in the docsite folder being touched - we're looking for the inverse of that in this task).