aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools/backport-pr.sh
Commit message (Expand)AuthorAge
* Add new options --no-conflict and --no-signature-check to backport script.Gravatar Théo Zimmermann2018-07-10
* 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