17b5d38 devtools: show pull and commit information in github-merge (Wladimir J. van der Laan)
da6d18b devtools: replace github-merge with python version (Wladimir J. van der Laan)