ci: skip remote documentation generation on PRs

The remote documentation step fetches and builds develop, master, and
all tags. This content is unrelated to the PR and is only needed for
website publishing.

The local documentation step (which builds only HEAD) still runs and
validates that the PR does not break doc generation.

Author: gennaroprota

.github/workflows/ci.yml

@@ -996,6 +996,10 @@ jobs:
             '+refs/tags/*:refs/tags/*'
 
       - name: Generate Remote Documentation
+        # This step fetches and builds develop, master and all tags. That's
+        # unrelated to a PR, and is only needed for website publishing. So, skip
+        # for a PR.
+        if: github.event_name != 'pull_request'
         working-directory: docs
         run: |
           # This playbook renders the documentation