Merge pull request #6018 from simonpasquier/delete-remote-makefile-common-branch

scripts/sync_makefiles.sh: delete merged branch

scripts/sync_repo_files.sh

@@ -39,6 +39,9 @@ fetch_repos() {
 push_branch() {
   # stdout and stderr are redirected to /dev/null otherwise git-push could leak
   # the token in the logs.
+  # Delete the remote branch in case it was merged but not deleted.
+  git push --quiet "https://${GITHUB_TOKEN}:@github.com/${1}" \
+    ":${branch}" 1>/dev/null 2>&1
   git push --quiet \
     "https://${GITHUB_TOKEN}:@github.com/${1}" \
     --set-upstream "${branch}" 1>/dev/null 2>&1
@@ -121,6 +124,16 @@ for org in ${orgs}; do
   # at most but it should be enough for us as there are less than 40 repositories
   # currently.
   fetch_repos "${org}" | while read -r repo; do
+    # Check if a PR is already opened for the branch.
+    prLink=$(curl --show-error --silent \
+      -u "${GITHUB_USER}:${GITHUB_TOKEN}" \
+      "https://api.github.com/repos/${org}/${repo}/pulls?head=${repo}:${branch}" | jq '.[0].url')
+    if [[ "${prLink}" != "null" ]]; then
+      echo "Pull request already opened for branch '${branch}': ${prLink}"
+      echo "Either close it or merge it before running this script again!"
+      continue
+    fi
+
     if ! process_repo "${org}/${repo}"; then
       echo "Failed to process '${org}/${repo}'"
       exit 1