diff options
Diffstat (limited to 'dev/ci/ci-common.sh')
| -rw-r--r-- | dev/ci/ci-common.sh | 39 |
1 files changed, 21 insertions, 18 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 58c90ff11..1838db5d0 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,16 @@ 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} +# shellcheck source=ci-basic-overlay.sh +source "${ci_dir}/ci-basic-overlay.sh" +for overlay in "${ci_dir}"/user-overlays/*.sh; do + # shellcheck source=/dev/null + source "${overlay}" done -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 +48,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 +82,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 && \ |