Piotr Sarna e8871181eb scripts: add a script for pulling GitHub pull requests ...

In order to avoid the UI merge button which tends to
mess up commit authors, a simple script for pulling
a PR from GitHub is added.
Example usage:
 $ git fetch; git checkout origin/next
 $ ./scripts/pull_github_pr.sh 6007

Message-Id: <1fa79c8be47b5660fc24a81fc0ab381aa26d98af.1584014944.git.sarna@scylladb.com>

2020-03-12 21:37:05 +01:00

1006 B

Executable File

Raw Blame History

View Raw