2 commits

Author	SHA1	Message	Date
Wladimir J. van der Laan	17b5d3896f	devtools: show pull and commit information in github-merge ... Print the number and title of the pull, as well as the commits to be merged.	2016-01-22 16:37:42 +01:00
Wladimir J. van der Laan	da6d18b6c7	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	2016-01-20 13:02:45 +01:00