scripts/pull_github_pr.sh: don't guess git remote name

The script assumes the remote name is "origin", a fair
assumption, but not universally true. Read it from configuration
instead of guessing it.

Closes #9423
This commit is contained in:
Avi Kivity
2021-10-03 18:10:09 +03:00
committed by Nadav Har'El
parent 414b672e22
commit 93b765f655

View File

@@ -25,7 +25,10 @@ NL=$'\n'
PR_NUM=$1
# convert full repo URL to its project/repo part:
PROJECT=`git config --get remote.origin.url | sed 's/git@github.com://;s#https://github.com/##;s/\.git$//;'`
REMOTE_SLASH_BRANCH="$(git rev-parse --abbrev-ref --symbolic-full-name @{upstream})"
REMOTE="${REMOTE_SLASH_BRANCH%/*}"
REMOTE_URL="$(git config --get "remote.$REMOTE.url")"
PROJECT=`sed 's/git@github.com://;s#https://github.com/##;s/\.git$//;' <<<"${REMOTE_URL}"`
PR_PREFIX=https://api.github.com/repos/$PROJECT/pulls
echo "Fetching info on PR #$PR_NUM... "
@@ -45,7 +48,7 @@ echo -n "Fetching full name of author $PR_LOGIN... "
USER_NAME=$(curl -s "https://api.github.com/users/$PR_LOGIN" | jq -r .name)
echo "$USER_NAME"
git fetch origin pull/$PR_NUM/head
git fetch "$REMOTE" pull/$PR_NUM/head
nr_commits=$(git log --pretty=oneline HEAD..FETCH_HEAD | wc -l)