Cleanup shell expansions and quoting.

2 files changed, 29 insertions, 28 deletions

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 58c90ff11..676edb740 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -4,7 +4,7 @@ set -xe
 
 if [ -n "${GITLAB_CI}" ];
 then
-    export COQBIN=`pwd`/_install_ci/bin
+    export COQBIN="$PWD/_install_ci/bin"
     export CI_BRANCH="$CI_COMMIT_REF_NAME"
 else
     if [ -n "${TRAVIS}" ];
@@ -16,7 +16,7 @@ else
         export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
         export CI_BRANCH="$CIRCLE_BRANCH"
     fi
-    export COQBIN=`pwd`/bin
+    export COQBIN="$PWD/bin"
 fi
 export PATH="$COQBIN:$PATH"
 
@@ -26,14 +26,14 @@ export COQBIN="$COQBIN/"
 ls "$COQBIN"
 
 # Where we clone and build external developments
-CI_BUILD_DIR=`pwd`/_build_ci
+CI_BUILD_DIR="$PWD/_build_ci"
 
-for overlay in ${ci_dir}/user-overlays/*.sh; do
-  source ${overlay}
+for overlay in "${ci_dir}"/user-overlays/*.sh; do
+  source "${overlay}"
 done
-source ${ci_dir}/ci-basic-overlay.sh
+source "${ci_dir}/ci-basic-overlay.sh"
 
-mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
+mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"
 
 # git_checkout branch url dest will create a git repository
 # in <dest> (if it does not exist already) and checkout the
@@ -46,15 +46,16 @@ git_checkout()
 
   # Allow an optional 4th argument for the commit
   local _COMMIT=${4:-FETCH_HEAD}
-  local _DEPTH=$(if [ -z "${4}" ]; then echo "--depth 1"; fi)
-
-  mkdir -p ${_DEST}
-  ( cd ${_DEST}                                                && \
-    if [ ! -d .git ] ; then git clone ${_DEPTH} ${_URL} . ; fi && \
-    echo "Checking out ${_DEST}"                               && \
-    git fetch ${_URL} ${_BRANCH}                               && \
-    git checkout ${_COMMIT}                                    && \
-    echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
+  local _DEPTH=()
+  if [ -z "${4}" ]; then _DEPTH=(--depth 1); fi
+
+  mkdir -p "${_DEST}"
+  ( cd "${_DEST}"                                                     && \
+    if [ ! -d .git ] ; then git clone "${_DEPTH[@]}" "${_URL}" . ; fi && \
+    echo "Checking out ${_DEST}"                                      && \
+    git fetch "${_URL}" "${_BRANCH}"                                  && \
+    git checkout "${_COMMIT}"                                         && \
+    echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" )
 }
 
 checkout_mathcomp()
@@ -79,8 +80,8 @@ install_ssreflect()
 {
   echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
 
-  checkout_mathcomp ${mathcomp_CI_DIR}
-  ( cd ${mathcomp_CI_DIR}/mathcomp   && \
+  checkout_mathcomp "${mathcomp_CI_DIR}"
+  ( cd "${mathcomp_CI_DIR}/mathcomp" && \
     sed -i.bak '/ssrtest/d'     Make && \
     sed -i.bak '/odd_order/d'   Make && \
     sed -i.bak '/all\/all.v/d'  Make && \
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 0c4a79bfd..9c52644c6 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -9,18 +9,18 @@ set -e
 
 PR=$1
 
-CURRENT_LOCAL_BRANCH=`git rev-parse --abbrev-ref HEAD`
-REMOTE=`git config --get branch.$CURRENT_LOCAL_BRANCH.remote`
-git fetch $REMOTE refs/pull/$PR/head
+CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
+REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote")
+git fetch "$REMOTE" "refs/pull/$PR/head"
 
 API=https://api.github.com/repos/coq/coq
 
-BASE_BRANCH=`curl -s $API/pulls/$PR | jq -r '.base.label'`
+BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label')
 
-COMMIT=`git rev-parse FETCH_HEAD`
-STATUS=`curl -s $API/commits/$COMMIT/status | jq -r '.state'`
+COMMIT=$(git rev-parse FETCH_HEAD)
+STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state')
 
-if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then
+if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then
   echo "Wrong base branch"
   read -p "Bypass? [y/N] " -n 1 -r
   echo
@@ -30,7 +30,7 @@ if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then
   fi
 fi;
 
-if [ $STATUS != "success" ]; then
+if [ "$STATUS" != "success" ]; then
   echo "CI status is \"$STATUS\""
   read -p "Bypass? [y/N] " -n 1 -r
   echo
@@ -40,10 +40,10 @@ if [ $STATUS != "success" ]; then
   fi
 fi;
 
-git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e
+git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $(curl -s "$API/pulls/$PR" | jq -r '.title')" -e
 
 # TODO: improve this check
-if [[ `git diff $REMOTE/$CURRENT_LOCAL_BRANCH dev/ci` ]]; then
+if [[ $(git diff "$REMOTE/$CURRENT_LOCAL_BRANCH" dev/ci) ]]; then
   echo "******************************************"
   echo "** WARNING: does this PR have overlays? **"
   echo "******************************************"