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 | |
---|---|---|
.. | ||
devtools | 8 years ago | |
verify-commits | 8 years ago | |
README.md | 8 years ago |
README.md
Repository Tools
Developer tools
Specific tools for developers working on this repository.
Contains the script github-merge.py
for merging github pull requests securely and signing them using GPG.
Verify-Commits
Tool to verify that every merge commit was signed by a developer using the above github-merge.py
script.