aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools/merge-pr.sh
Commit message (Expand)AuthorAge
* This script apparently uses bash-specific features.Gravatar Théo Zimmermann2017-11-29
* Fix PR merge script.Gravatar Théo Zimmermann2017-11-29
* Add PR merge script.Gravatar Maxime Dénès2017-11-28