From 7e1f33b716e02ceb06e325b1f81812417bf081a1 Mon Sep 17 00:00:00 2001
From: Laurent Rineau <Laurent.Rineau@cgal.org>
Date: Thu, 20 Jun 2024 16:57:53 +0200
Subject: [PATCH] Fix build_doc.yml

Checkout `refs/pull/$PR/head` instead of `refs/pull/$PR/merge`.

If the pull-request has conflicts, that is different.
---
 .github/workflows/build_doc.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/build_doc.yml b/.github/workflows/build_doc.yml
index 9735cd3d3c8..53f673c203d 100644
--- 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