index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
dev
/
tools
/
merge-pr.sh
Age
Commit message (
Expand
)
Author
2018-06-09
[merge script] Check if the CI that was run is outdated.
Théo Zimmermann
2018-04-11
merge script support https + typos in doc
Pierre Courtieu
2018-04-09
Merge script: adds a way for confirmation to expect a newline.
Théo Zimmermann
2018-04-09
Add sanity check in merge script: local branch is up-to-date.
Théo Zimmermann
2018-04-08
Document requirement to have git >= 2.7 to use the merge script.
Théo Zimmermann
2018-04-08
Merge script does not warn when the remote is set to HTTPS.
Théo Zimmermann
2018-04-08
Merge script: use fetch URL for the remote.
Théo Zimmermann
2018-04-05
Improve shell scripts
zapashcanon
2018-04-03
merge-pr.sh: cache github API calls
Gaëtan Gilbert
2018-03-23
improve merge-pr script
Enrico Tassi
2018-01-16
merge-pr.sh: use git diff --quiet
Gaëtan Gilbert
2018-01-16
Cleanup shell expansions and quoting.
Gaëtan Gilbert
2017-11-29
This script apparently uses bash-specific features.
Théo Zimmermann
2017-11-29
Fix PR merge script.
Théo Zimmermann
2017-11-28
Add PR merge script.
Maxime Dénès
