diff options
| author |  zapashcanon <leo@ndrs.fr> | 2018-02-21 22:42:10 +0100 |
|---|---|---|
| committer | zapashcanon <leo@ndrs.fr> | 2018-04-05 22:05:43 +0100 |
| commit | 250502b01340ec6bedace85c6a2d4a4e57a107cf (patch) | |
| tree | 256fd7d0e38d2bdc24350eb18e61b0fb73e44215 /dev/ci/ci-common.sh | |
| parent | b7938d0a51cdef8076bf5e1a58907b845a3fcc3d (diff) | |
Improve shell scripts
Diffstat (limited to 'dev/ci/ci-common.sh')
| -rw-r--r-- | dev/ci/ci-common.sh | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index d7a356930..189734a0b 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -20,7 +20,8 @@ else export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" export CI_BRANCH="$CIRCLE_BRANCH" else # assume local - export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" + CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" + export CI_BRANCH fi export COQBIN="$PWD/bin" fi @@ -35,10 +36,10 @@ ls "$COQBIN" CI_BUILD_DIR="$PWD/_build_ci" # shellcheck source=ci-basic-overlay.sh -source "${ci_dir}/ci-basic-overlay.sh" +. "${ci_dir}/ci-basic-overlay.sh" for overlay in "${ci_dir}"/user-overlays/*.sh; do # shellcheck source=/dev/null - source "${overlay}" + . "${overlay}" done mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" @@ -68,7 +69,7 @@ git_checkout() checkout_mathcomp() { - git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1} + git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${1}" } make() |