diff options
| author | Maxime Dénès | 2018-04-19 13:35:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-04-19 13:35:29 +0200 |
| commit | 9a4ca53a3a021cb16de7706ec79a26e49f54de49 (patch) | |
| tree | b1d6a2f65920cdc7e00b5705855bab83ac484113 /dev/tools | |
| parent | d799b6a6117258583919dc4e518afd92b23a05ed (diff) | |
| parent | d1d67a41cad8723815403533dee161c0e4a42c59 (diff) | |
Merge PR #7219: 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 1c94f630f2..00d04e6b3d 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" |