[CI] Run DocsBuild only when needed

Oftentimes pushes to branches and PRs doesn't change anything in docs/
or include/ directories which influence the documentation build. This
job takes ca. 1 minute to run with each push, so it's optimal to run it
only when relevant changes were made.

Also, there is no need for other pr_push jobs to wait for docs to build.
Developer can work on the docs and project build/tests in any order.

Author: PatKamin

.github/workflows/docs_pr_push.yml

@@ -0,0 +1,25 @@
+name: Documentation PR/push
+# debug
+on:
+  push:
+    branches-ignore:
+      - 'dependabot/**'
+      - 'main'  # Ignore main branch as it's handled by docs.yml
+    paths:
+      - 'docs/**'
+      - 'include/**'
+  pull_request:
+    paths:
+      - 'docs/**'
+      - 'include/**'
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  DocsBuild:
+    uses: ./.github/workflows/reusable_docs_build.yml

.github/workflows/pr_push.yml

@@ -18,11 +18,9 @@ permissions:
 jobs:
   CodeChecks:
     uses: ./.github/workflows/reusable_checks.yml
-  DocsBuild:
-    uses: ./.github/workflows/reusable_docs_build.yml
   FastBuild:
     name: Fast builds
-    needs: [CodeChecks, DocsBuild]
+    needs: [CodeChecks]
     uses: ./.github/workflows/reusable_fast.yml
   Build:
     name: Basic builds