Fix build_doc.yml

Checkout `refs/pull/$PR/head` instead of `refs/pull/$PR/merge`. If the pull-request has conflicts, that is different.
CGAL · Jun 20, 2024 · 7e1f33b · 7e1f33b
1 parent 9075f96
commit 7e1f33b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/workflows/build_doc.yml b/.github/workflows/build_doc.yml
@@ -65,7 +65,7 @@ jobs:
         if: steps.get_round.outputs.result != 'stop'
         with:
            repository: ${{ github.repository }}
-           ref: refs/pull/${{ steps.get_pr_number.outputs.result }}/merge
+           ref: refs/pull/${{ steps.get_pr_number.outputs.result }}/head
            fetch-depth: 2
 
       - name: install dependencies