feat: improve pr doc deployment with labelling strategy

Author: moe-ad

.github/labeler.yml

@@ -15,4 +15,12 @@ dependencies:
 CI/CD:
 - docker/**/*
 - .github/**/*
-- .ci/**/*
+- .ci/**/*
+
+# HACK: the label is declared with the only purpose of avoiding the
+# GitHub labeler bot from removing it. This is a known issue reported in the
+# official action/labeler repo https://github.com/actions/labeler/issues/763
+'deploy-pr-doc':
+  - all:
+      - changed-files:
+          - all-globs-to-all-files: ['THIS-NEVER-MATCHES-A-FILE']

.github/labels.yml

@@ -0,0 +1,3 @@
+- name: 'deploy-pr-doc'
+  description: Deploy pull request documentation
+  color: 00ff00

.github/workflows/ci.yml

@@ -2,7 +2,7 @@ name: CI
 
 on:
   pull_request:
-    types: [opened, synchronize, reopened, ready_for_review, closed]
+    types: [opened, synchronize, reopened, ready_for_review, closed, labeled]
     branches-ignore:
       - '*no-ci*'
   push:
@@ -159,7 +159,10 @@ jobs:
     name: "Deploy PR documentation"
     runs-on: ubuntu-latest
     needs: docs
-    if: always() && (needs.docs.result == 'success' || needs.docs.result == 'skipped')
+    if: |
+      always() &&
+      (needs.docs.result == 'success' || needs.docs.result == 'skipped') &&
+      contains(github.event.pull_request.labels.*.name, 'deploy-pr-doc')
     steps:
       - uses: ansys/actions/doc-deploy-pr@v10
         with: