Don't run docs build job on every push to PR #1232
Description
Rationale
All other jobs have to wait for the DocsBuild job to finish which is an overhead in the CI.
Description
The DocsBuild job is one of two jobs that blocks the bulk of CI from running when called from the pr_push.yml workflow. As I agree that one of them, CodeChecks, is rightfully blocking the rest of CI until passed, waiting for DocsBuild is an unnecessary overhead added on each and every PR push.
Running this job only for changes in include/ and docs/ directories would be sufficient.
Implementation details
A possible change would be to move the DocsBuild call from the PR/push workflow to the separate new workflow called on each PR push that actually edits either include/ or docs/ directories. Therefore, also remove the wait for this job to complete in order to run the bulk of the CI.