aboutsummaryrefslogtreecommitdiff
path: root/contrib/devtools/github-merge.py
AgeCommit message (Expand)Author
2016-01-25Merge #7402: [devtools] github-merge get toplevel dir without extra whitespaceWladimir J. van der Laan
2016-01-25[devtools] github-merge get toplevel dir without extra whitespaceAndrew C
2016-01-22devtools: show pull and commit information in github-mergeWladimir J. van der Laan
2016-01-20devtools: replace github-merge with python versionWladimir J. van der Laan