From 7d3e3f0aa5aea66a5e3c884eb0642a317d762051 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 28 Mar 2018 16:56:37 +0200
Subject: Merge script: use fetch URL for the remote.

In case the push URL has been overriden to make it fetch-only.
---
 dev/tools/merge-pr.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/tools')

diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 20612eeb85..aa83c626e3 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -79,7 +79,7 @@ if [ -z "$REMOTE" ]; then
   error "please run: git branch --set-upstream-to=THE_REMOTE/$CURRENT_LOCAL_BRANCH"
   exit 1
 fi
-REMOTE_URL=$(git remote get-url "$REMOTE" --push)
+REMOTE_URL=$(git remote get-url "$REMOTE" --all)
 if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" ] && \
    [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then
   error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo"
-- 
cgit v1.2.3