From 250502b01340ec6bedace85c6a2d4a4e57a107cf Mon Sep 17 00:00:00 2001
From: zapashcanon <leo@ndrs.fr>
Date: Wed, 21 Feb 2018 22:42:10 +0100
Subject: Improve shell scripts

---
 dev/tools/backport-pr.sh | 10 +++++-----
 dev/tools/merge-pr.sh    |  4 ++--
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'dev/tools')

diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index e4359f703..5205350a6 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -27,9 +27,9 @@ BRANCH=backport-pr-${PRNUM}
 RANGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%P" | sed 's/ /../')
 MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merge/Backport/')
 
-if git checkout -b ${BRANCH}; then
+if git checkout -b "${BRANCH}"; then
 
-    if ! git cherry-pick -x ${RANGE}; then
+    if ! git cherry-pick -x "${RANGE}"; then
         echo "Please fix the conflicts, then exit."
         bash
         while ! git cherry-pick --continue; do
@@ -50,7 +50,7 @@ else
 
 fi
 
-if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then
+if ! git diff --exit-code HEAD "${BRANCH}" -- "*.mli"; then
     echo
     read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r
     echo
@@ -63,8 +63,8 @@ if [[ "${OPTION}" == "--stop-before-merging" ]]; then
     exit 0
 fi
 
-git merge -S --no-ff ${BRANCH} -m "${MESSAGE}"
-git branch -d ${BRANCH}
+git merge -S --no-ff "${BRANCH}" -m "${MESSAGE}"
+git branch -d "${BRANCH}"
 
 # To-Do:
 # - Support for backporting a PR before it is merged
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index ecfdfab94..20612eeb8 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