diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/MERGING.md | 2 | ||||
| -rwxr-xr-x | dev/tools/merge-pr.sh | 8 |
2 files changed, 6 insertions, 4 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 3a2df6a81..84ff94c66 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -70,7 +70,7 @@ To merge the PR proceed in the following way ``` $ git checkout master $ git pull -$ dev/tools/merge-pr XXXX +$ dev/tools/merge-pr.sh XXXX $ git push upstream ``` where `XXXX` is the number of the PR to be merged and `upstream` is the name diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 1c94f630f..00d04e6b3 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -5,7 +5,7 @@ set -o pipefail 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" +OFFICIAL_REMOTE_HTTPS_URL="github.com/coq/coq" # This script depends (at least) on git (>= 2.7) and jq. # It should be used like this: dev/tools/merge-pr.sh /PR number/ @@ -91,8 +91,10 @@ fi REMOTE_URL=$(git remote get-url "$REMOTE" --all) if [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}" ] && \ [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}.git" ] && \ - [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_HTTPS_URL}" ] && \ - [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_HTTPS_URL}.git" ]; then + [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}" ] && \ + [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}.git" ] && \ + [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}" ]] && \ + [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}.git" ]] ; then error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo" error "that is ${BLUE}$OFFICIAL_REMOTE_GIT_URL" error "it points to ${BLUE}$REMOTE_URL${RESET} instead" |