aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools/backport-pr.sh
Commit message (Collapse)AuthorAge
* Improve shell scriptsGravatar zapashcanon2018-04-05
|
* [Backport script] Check .mli files are not changed.Gravatar Théo Zimmermann2018-01-09
|
* Update backport script for more control.Gravatar Théo Zimmermann2017-12-24
|
* Fix usage comment.Gravatar Théo Zimmermann2017-11-29
|
* Add PR backport script.Gravatar Théo Zimmermann2017-11-28