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 deadalnix Pushed on May 14 2017, 22:04 - Parents
- rABC17b5d3896f2c: devtools: show pull and commit information in github-merge
rABC9f796f3d2b53: Merge #7400: Add achow101's pgp key - Branches
- Unknown
- Tags
Merged Changes
Merged Changes