aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/merge-pr.sh
AgeCommit message (Expand)Author
2018-01-16merge-pr.sh: use git diff --quietGaëtan Gilbert
2018-01-16Cleanup shell expansions and quoting.Gaëtan Gilbert
2017-11-29This script apparently uses bash-specific features.Théo Zimmermann
2017-11-29Fix PR merge script.Théo Zimmermann
2017-11-28Add PR merge script.Maxime Dénès