diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-04-11 11:08:23 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-04-11 15:03:34 +0200 |
| commit | d1d67a41cad8723815403533dee161c0e4a42c59 (patch) | |
| tree | 94b526f0e32a7d133c6ad2c881ad8deba1b6d4d7 /dev/tools | |
| parent | 8059a0efa79fcd72d56c424adf1bea10dae28d6d (diff) | |
merge script support https + typos in doc
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/merge-pr.sh | 8 |
1 files changed, 5 insertions, 3 deletions
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" |