From 250502b01340ec6bedace85c6a2d4a4e57a107cf Mon Sep 17 00:00:00 2001
From: zapashcanon
Date: Wed, 21 Feb 2018 22:42:10 +0100
Subject: Improve shell scripts

---
 dev/tools/merge-pr.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev/tools/merge-pr.sh')

diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index ecfdfab948..20612eeb85 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -80,8 +80,8 @@ if [ -z "$REMOTE" ]; then
   exit 1
 fi
 REMOTE_URL=$(git remote get-url "$REMOTE" --push)
-if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" -a \
-     "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then
+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"
   error "that is ${BLUE}$OFFICIAL_REMOTE_URL"
   error "it points to ${BLUE}$REMOTE_URL${RESET} instead"
-- 
cgit v1.2.3