diff --git a/scripts/sync_repo_files.sh b/scripts/sync_repo_files.sh index 560ad812b..4d2f47866 100755 --- a/scripts/sync_repo_files.sh +++ b/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 @@ -119,6 +122,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