Wladimir J. van der Laan
6a5932bf2a
Merge #7402 : [devtools] github-merge get toplevel dir without extra whitespace
...
5ed2f16
[devtools] github-merge get toplevel dir without extra whitespace (Andrew C)
2016-01-25 15:42:16 +01:00
Andrew C
5ed2f16480
[devtools] github-merge get toplevel dir without extra whitespace
...
Fixes a bug in github merge when it runs the tests where the toplevel directory has an extra '\n' appended to the path string. Now it doesn't.
2016-01-25 09:02:05 -05:00
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