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|
|devtools||5 years ago|
|verify-commits||5 years ago|
|README.md||5 years ago|
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.
Tool to verify that every merge commit was signed by a developer using the above