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

10 KiB

Executable File

Raw Blame History

View Raw