| Age | Commit message (Collapse) | 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-26 | Improve the backport script. | Guillaume Melquiond | |
| It now uses the origin/master branch rather than the master branch, thus avoiding the need for local merges. More importantly, it no longer creates a subshell in case of conflicts, but instead gives control back to the user. Once conflicts are solved, it suffices to relaunch the script (instead of exiting the subshell). The reason is that, otherwise, there was no sane way of giving up a backport, due to the infinite subshell loop. | |||
| 2018-07-10 | Add new options --no-conflict and --no-signature-check to backport script. | Théo Zimmermann | |
| 2018-04-05 | Improve shell scripts | zapashcanon | |
| 2018-01-09 | [Backport script] Check .mli files are not changed. | Théo Zimmermann | |
| 2017-12-24 | Update backport script for more control. | Théo Zimmermann | |
| 2017-11-29 | Fix usage comment. | Théo Zimmermann | |
| 2017-11-28 | Add PR backport script. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |