index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
dev
/
tools
/
merge-pr.sh
Commit message (
Expand
)
Author
Age
*
[merge script] Check if the CI that was run is outdated.
Théo Zimmermann
2018-06-09
*
merge script support https + typos in doc
Pierre Courtieu
2018-04-11
*
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-09
*
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-08
*
Improve shell scripts
zapashcanon
2018-04-05
*
merge-pr.sh: cache github API calls
Gaëtan Gilbert
2018-04-03
*
improve merge-pr script
Enrico Tassi
2018-03-23
*
merge-pr.sh: use git diff --quiet
Gaëtan Gilbert
2018-01-16
*
Cleanup shell expansions and quoting.
Gaëtan Gilbert
2018-01-16
*
This script apparently uses bash-specific features.
Théo Zimmermann
2017-11-29
*
Fix PR merge script.
Théo Zimmermann
2017-11-29
*
Add PR merge script.
Maxime Dénès
2017-11-28