aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/merge-pr.sh
AgeCommit message (Expand)Author
2019-02-21Merge PR #9388: merge-pr.sh: fix #9387: quick_conf doesn't work in emacs shel...Emilio Jesus Gallego Arias
2019-02-04Remove AppVeyor: superseded by Azure.Théo Zimmermann
2019-01-23merge-pr.sh: fix #9387: quick_conf doesn't work in emacs shell bufferGaëtan Gilbert
2019-01-22Remove travisGaëtan Gilbert
2019-01-17Fix merge-pr.sh when multiple review commentsGaëtan Gilbert
2019-01-08merge-pr: add reviewer info to commit messageGaëtan Gilbert
2018-11-18merge-pr: Improve overlay checkGaëtan Gilbert
2018-06-09[merge script] Check if the CI that was run is outdated.Théo Zimmermann
2018-04-11merge script support https + typos in docPierre Courtieu
2018-04-09Merge script: adds a way for confirmation to expect a newline.Théo Zimmermann
2018-04-09Add sanity check in merge script: local branch is up-to-date.Théo Zimmermann
2018-04-08Document requirement to have git >= 2.7 to use the merge script.Théo Zimmermann
2018-04-08Merge script does not warn when the remote is set to HTTPS.Théo Zimmermann
2018-04-08Merge script: use fetch URL for the remote.Théo Zimmermann
2018-04-05Improve shell scriptszapashcanon
2018-04-03merge-pr.sh: cache github API callsGaëtan Gilbert
2018-03-23improve merge-pr scriptEnrico Tassi
2018-01-16merge-pr.sh: use git diff --quietGaëtan Gilbert
2018-01-16Cleanup shell expansions and quoting.Gaëtan Gilbert
2017-11-29This script apparently uses bash-specific features.Théo Zimmermann
2017-11-29Fix PR merge script.Théo Zimmermann
2017-11-28Add PR merge script.Maxime Dénès