ddf83f6ddc
After 93b765f655, our pull_github_pr.sh script tries to detect
a non-orthodox remote repo name, but it also adds an assumption
which breaks on some configurations (by some I mean mine).
Namely, the script tries to parse the repo name from the upstream
branch, assuming that current HEAD actually points to a branch,
which is not the way some users (by some I mean me) work with
remote repositories. Therefore, to make the script also work
with detached HEAD, it now has two fallback mechanisms:
1. If parsing @{upstream} failed, the script tries to parse
master@{upstream}, under the assumption that the master branch
was at least once used to track the remote repo.
2. If that fails, `origin/master` is used as last resort solution.
This patch allows some users (guess who) to get back to using
scripts/pull_github_pr.sh again without using a custom patched version.
Closes #10773
2.5 KiB
Executable File
2.5 KiB
Executable File