devtools: replace github-merge with python version

This is meant to be a direct translation of the bash script,
with the difference that it retrieves the PR title from github,
thus creating pull messages like:

    Merge #12345: Expose transaction temperature over RPC
This commit is contained in:
Wladimir J. van der Laan committed 2016-01-20 13:02:45 +01:00
1 parent 668906fcf2
commit da6d18b6c7
4 files changed
+227 -189

No files matched your search

+2 -2
View File
@@ -11,10 +11,10 @@ Repository Tools
### [Developer tools](/contrib/devtools) ###
Specific tools for developers working on this repository.
Contains the script `github-merge.sh` for merging github pull requests securely and signing them using GPG.
Contains the script `github-merge.py` for merging github pull requests securely and signing them using GPG.
### [Verify-Commits](/contrib/verify-commits) ###
Tool to verify that every merge commit was signed by a developer using the above `github-merge.sh` script.
Tool to verify that every merge commit was signed by a developer using the above `github-merge.py` script.
### [Linearize](/contrib/linearize) ###
Construct a linear, no-fork, best version of the blockchain.