From e9c84037e58a0c68913c01cdf581a5a5524f659f Mon Sep 17 00:00:00 2001
From: Laurent Rineau <laurent.rineau@cgal.org>
Date: Mon, 23 Sep 2024 12:18:48 +0200
Subject: [PATCH] try to fix build_doc [skip ci]

---
 .github/workflows/build_doc.yml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/build_doc.yml b/.github/workflows/build_doc.yml
index ba15781ddeb..7bc426e252e 100644
--- a/.github/workflows/build_doc.yml
+++ b/.github/workflows/build_doc.yml
@@ -32,6 +32,7 @@ jobs:
     runs-on: ubuntu-latest
     name: Checks if the workflow should be executed
     outputs:
+      trigger_build: ${{ steps.get_doc_version.outputs.result && steps.get_doc_version.outputs.result != '' }}
       force_build: ${{ steps.check_comment_body.outputs.force_build }}
       pr_number: ${{ steps.get_pr_number.outputs.pr_number }}
       doc_version: ${{ steps.get_doc_version.outputs.result }}
@@ -53,24 +54,27 @@ jobs:
             exit 1
           fi
           echo "force_build=${force_build}" >> $GITHUB_OUTPUT
+          echo "trigger_build=${trigger_build}" >> $GITHUB_OUTPUT
 
       - name: Check permissions
-        if: inputs.pr_number || env.author_association == 'OWNER' || env.author_association == 'MEMBER'
+        if: ${{ fromJSON(steps.check_comment_body.outputs.trigger_build) }} && (inputs.pr_number || env.author_association == 'OWNER' || env.author_association == 'MEMBER')
         run: echo "Authorized"
 
       - name: No permissions
-        if: ${{ ! inputs.pr_number && env.author_association != 'OWNER' && env.author_association != 'MEMBER' }}
+        if: ${{ fromJSON(steps.check_comment_body.outputs.trigger_build) }} && (! inputs.pr_number && env.author_association != 'OWNER' && env.author_association != 'MEMBER' )
         run: |
-          echo "Not Authorized"
+          echo 'ERROR: User ${{ github.actor }} is not allowed to trigger the build of the documentation with /build:* or /force-build:*'
           exit 1
 
       - name: Get PR number
+        if: ${{ fromJSON(steps.check_comment_body.outputs.trigger_build) }}
         id: get_pr_number
         env:
           pr_number: ${{ inputs.pr_number || github.event.issue.number }}
         run: echo "pr_number=$pr_number" >> $GITHUB_OUTPUT
 
       - name: Get doc version
+        if: ${{ fromJSON(steps.check_comment_body.outputs.trigger_build) }}
         uses: actions/github-script@v7
         id: get_doc_version
         with:
@@ -98,6 +102,7 @@ jobs:
       force_build: ${{ needs.pre_build_checks.outputs.force_build }}
       pr_number: ${{ needs.pre_build_checks.outputs.pr_number }}
       doc_version: ${{ needs.pre_build_checks.outputs.doc_version }}
+    if: ${{ fromJSON(needs.pre_build_checks.outputs.trigger_build) }}
     steps:
 
       - name: Emoji-comment