diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-08 20:19:18 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-08 20:46:10 +0200 |
| commit | ff223fac386ab4d0e622d1dc03d47cff34db3311 (patch) | |
| tree | 666b974024c58f7384ccdef9bf8c689fe16756da /dev | |
| parent | e332bf0d9685679f4c5415bec7681fd948921fb5 (diff) | |
Document requirement to have git >= 2.7 to use the merge script.
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/tools/merge-pr.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 337fa43a3..c4ee2aa73 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -7,7 +7,7 @@ API=https://api.github.com/repos/coq/coq OFFICIAL_REMOTE_GIT_URL="git@github.com:coq/coq" OFFICIAL_REMOTE_HTTPS_URL="https://github.com/coq/coq" -# This script depends (at least) on git and jq. +# This script depends (at least) on git (>= 2.7) and jq. # It should be used like this: dev/tools/merge-pr.sh /PR number/ RED="\033[31m" |