Wladimir J. van der Laan
devtools: Auto-set branch to merge to in github-merge
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.
|5 years ago|
|README.md||5 years ago|
|github-merge.py||4 years ago|
This directory contains tools for developers working on this repository.
A small script to automate merging pull-requests securely and sign them with GPG.
(in any git repository) will help you merge pull request #3077 for the devrandom/gitian-builder repository.
What it does:
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.
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)