You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
e1a57442fd
As we are already using the API to retrieve the pull request title, also retrieve the base branch. This makes sure that pull requests for 0.12 automatically end up in 0.12, and pull requests for master automatically end up in master, and so on. It is still possible to override the branch from the command line or using the `githubmerge.branch` git option. |
8 years ago | |
|---|---|---|
| .. | ||
| README.md | 8 years ago | |
| github-merge.py | 8 years ago | |
README.md
Contents
This directory contains tools for developers working on this repository.
github-merge.py
A small script to automate merging pull-requests securely and sign them with GPG.
For example:
./github-merge.py 3077
(in any git repository) will help you merge pull request #3077 for the devrandom/gitian-builder repository.
What it does:
- Fetch master and the pull request.
- Locally construct a merge commit.
- Show the diff that merge results in.
- Ask you to verify the resulting source tree (so you can do a make check or whatever).
- Ask you whether to GPG sign the merge commit.
- Ask you whether to push the result upstream.
This means that there are no potential race conditions (where a pullreq gets updated while you're reviewing it, but before you click merge), and when using GPG signatures, that even a compromised github couldn't mess with the sources.
Setup
Configuring the github-merge tool for this repository is done in the following way:
git config githubmerge.repository devrandom/gitian-builder
git config githubmerge.testcmd "make -j4 check" (adapt to whatever you want to use for testing)
git config --global user.signingkey mykeyid (if you want to GPG sign)