devtools: show pull and commit information in github-merge
17b5d3896f2cUnpublished
Actions

Unpublished Commit · Learn More

Repository Importing: This repository is still importing.

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.

Provenance

Wladimir J. van der Laan <laanwj@gmail.com>	Authored on Jan 22 2016, 15:37
schancel	Pushed on Jan 5 2018, 21:58
schancel	Pushed on Jan 5 2018, 21:39
schancel	Pushed on Jan 5 2018, 21:17

Parents

Branches

Unknown

Tags

Unknown

Wladimir J. van der Laan <laanwj@gmail.com> committed rSTAGING17b5d3896f2c: devtools: show pull and commit information in github-merge (authored by Wladimir J. van der Laan <laanwj@gmail.com>).Jan 22 2016, 15:37

Path

Size

contrib/

devtools/