Avi Kivity 93b765f655 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

2021-10-04 12:32:39 +03:00

1.9 KiB

Executable File

Raw Blame History

View Raw