aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/backport-pr.sh
AgeCommit message (Expand)Author
2020-05-23[dev/tools] Fix #12314: do not die silently if branch has no remote.Théo Zimmermann
2020-05-22[backport-pr] Select correct remote of the master branch.Théo Zimmermann
2019-03-26Improve the backport script.Guillaume Melquiond
2018-07-10Add new options --no-conflict and --no-signature-check to backport script.Théo Zimmermann
2018-04-05Improve shell scriptszapashcanon
2018-01-09[Backport script] Check .mli files are not changed.Théo Zimmermann
2017-12-24Update backport script for more control.Théo Zimmermann
2017-11-29Fix usage comment.Théo Zimmermann
2017-11-28Add PR backport script.Théo Zimmermann