From 11b69df045a7f418c211f7bc2dcdda9c3c93681e Mon Sep 17 00:00:00 2001 From: Laurent Rineau Date: Wed, 17 Mar 2021 17:49:33 +0100 Subject: [PATCH] Fix tag_pr_per_release.sh to work with non-fast-forward updates --- Scripts/developer_scripts/tag_pr_per_release.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Scripts/developer_scripts/tag_pr_per_release.sh b/Scripts/developer_scripts/tag_pr_per_release.sh index a8927dcfe17..36e8c56e859 100644 --- a/Scripts/developer_scripts/tag_pr_per_release.sh +++ b/Scripts/developer_scripts/tag_pr_per_release.sh @@ -30,7 +30,7 @@ REMOTE=`git config branch.releases/CGAL-${PREVIOUS_MAJOR_RELEASE}-branch.remote # Call git-fetch to refresh the branch, and fetch the references # refs/pull/*/head as well. -git fetch --tags "${REMOTE}" `git config "remote.${REMOTE}.fetch"` 'refs/pull/*/head:refs/pull/*/head' +git fetch --tags "${REMOTE}" `git config --get-all "remote.${REMOTE}.fetch"` '+refs/pull/*/head:refs/pull/*/head' PR_LIST=`git log --pretty='%D' v${PREVIOUS_MAJOR_RELEASE}..v${CURRENT_RELEASE} | awk 'match($0, /refs\/pull\/([0-9]+)\/head/, a) {print a[1]}' | sort -u`