aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools/merge-pr.sh
Commit message (Collapse)AuthorAge
* This script apparently uses bash-specific features.Gravatar Théo Zimmermann2017-11-29
|
* Fix PR merge script.Gravatar Théo Zimmermann2017-11-29
| | | | Was still relying on the existence of user-configured /pr/.
* Add PR merge script.Gravatar Maxime Dénès2017-11-28