Pull Request #1247 Add script for merging a github pull request
Although github pull requests are convenient way to track pending
patches and to review small or large patch sets, it's not obvious
for maintainers how to try such PRs locally, and also when
eventually deciding to merge the PR, github provides a "merge"
button in its GUI with multiple problems:
1. It often botches the committer's address
2. It "merges" even single-patch PRs. This is not OSv's
tradition - single patches should remain a single patch,
not a merge of a single-patch branch.
The script in this patch, scripts/pull_github_pr.sh, solves
both problems: If the maintainer runs,
scripts/pull_github_pr.sh 1245
Fetches PR number 1245 locally, you can then compile and test
it yourself, and if you're pleased, finally push it.
A complete session may look something like this:
# get your working directory to modern master, as usual
git checkout master
git pull
git submodule update --recursive
# Pull pull request 1245:
scripts/pull_github_pr.sh 1245
# Now maybe compile OSv, test, it, and so on.
# When you're pleased, and want to merge the PR, do:
git push
This script is based on a similar script from the Scylla project.
The script works slightly differently for single-patch vs.
multiple-patch PRs:
1. For a multiple-patch PR, the PR branch is merged. The
first comment in the PR is used as the content of the
merge commit so PR authors should edit this first comment
to have good content.
When this is merged into master, github automatically
closes the PR as "merged".
2. For a single-patch PR, the PR branch is *not* merged,
instead the single patch is pushed as a single patch.
Github doesn't realise that the branch was "merged"
so instead the script adds a "Closes" tag to the
commit message so that the PR is closed automatically
when the result is merged.
Signed-off-by: Nadav Har'El <nyh@scylladb.com>