Wladimir J. van der Laan 7dfa83448d 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.

2018-11-09 22:51:06 +03:00

10 KiB

Executable File

Raw Blame History

View Raw