aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools/merge-pr.sh
Commit message (Expand)AuthorAge
* [merge script] Check if the CI that was run is outdated.Gravatar Théo Zimmermann2018-06-09
* merge script support https + typos in docGravatar Pierre Courtieu2018-04-11
* Merge script: adds a way for confirmation to expect a newline.Gravatar Théo Zimmermann2018-04-09
* Add sanity check in merge script: local branch is up-to-date.Gravatar Théo Zimmermann2018-04-09
* Document requirement to have git >= 2.7 to use the merge script.Gravatar Théo Zimmermann2018-04-08
* Merge script does not warn when the remote is set to HTTPS.Gravatar Théo Zimmermann2018-04-08
* Merge script: use fetch URL for the remote.Gravatar Théo Zimmermann2018-04-08
* Improve shell scriptsGravatar zapashcanon2018-04-05
* merge-pr.sh: cache github API callsGravatar Gaëtan Gilbert2018-04-03
* improve merge-pr scriptGravatar Enrico Tassi2018-03-23
* merge-pr.sh: use git diff --quietGravatar Gaëtan Gilbert2018-01-16
* Cleanup shell expansions and quoting.Gravatar Gaëtan Gilbert2018-01-16
* This script apparently uses bash-specific features.Gravatar Théo Zimmermann2017-11-29
* Fix PR merge script.Gravatar Théo Zimmermann2017-11-29
* Add PR merge script.Gravatar Maxime Dénès2017-11-28