Merge #7395: devtools: show pull and commit information in github-merge
17b5d38 devtools: show pull and commit information in github-merge (Wladimir J. van der Laan)
Description
Description
Details
Details
- Provenance
Wladimir J. van der Laan <laanwj@gmail.com> Authored on Jan 25 2016, 13:58 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
- rSTAGING17b5d3896f2c: devtools: show pull and commit information in github-merge
rSTAGING9f796f3d2b53: Merge #7400: Add achow101's pgp key - Branches
- Unknown
- Tags
Merged Changes
Merged Changes