|
12345678910111213141516171819202122232425262728293031323334353637 |
- 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)
|
