aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/merge-pr.sh
AgeCommit message (Expand)Author
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