Build docs on PRs

* Build the docs in PRs that modify /docs/manuals folder contents.
* Only deploy the built docs if not building a PR.

.github/workflows/docs.yml

@@ -5,11 +5,16 @@ on:
     branches:
       - 4.2.x
     paths:
-     - "docs/manual/**"
+      - "docs/manual/**"
+  pull_request:
+    branches:
+      - 4.2.x
+    paths:
+      - "docs/manual/**"
   workflow_dispatch:
 
 jobs:
-  deploy:
+  deploy-docs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout GeoNetwork
@@ -24,7 +29,13 @@ jobs:
         run: pip install --upgrade pip && pip install -r docs/manual/requirements.txt
       - name: git configuration
         run: git config user.name 'github-actions[bot]' && git config user.email 'github-actions[bot]@users.noreply.github.com'
-      - name: deploy latest docs to gh-pages branch
+      - name: build docs without publishing them
+        if: ${{ github.event_name == 'pull_request' }}
+        working-directory: docs/manual
+        run: |
+          mike deploy --title "4.2 Stable" --no-redirect --update-aliases 4.2 stable
+      - name: deploy 4.2 docs to gh-pages branch
+        if: ${{ github.event_name != 'pull_request' }}
         working-directory: docs/manual
         run: |
           mike deploy --push --title "4.2 Stable" --no-redirect --update-aliases 4.2 stable