diff options
| author | Emilio Jesus Gallego Arias | 2019-02-18 19:36:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-18 19:36:27 +0100 |
| commit | fcc3ee5d3eed4703e88fc1a2f07006130b61d006 (patch) | |
| tree | 3f9fd5a85025d4e12db7a0484206e353e6dd695e /dev | |
| parent | ee6d8274483711f84277e449494c3a11a64dfea8 (diff) | |
| parent | 7e03019c888161cb027dd76c3fa393d3d8f442e5 (diff) | |
Merge PR #9597: [ci] Resolve commit corresponding to branch when downloading tarball.
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/ci-common.sh | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index a5aa54144c..b4d2a9ca4e 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -62,27 +62,30 @@ git_download() { local PROJECT=$1 local DEST="$CI_BUILD_DIR/$PROJECT" + local GITURL_VAR="${PROJECT}_CI_GITURL" + local GITURL="${!GITURL_VAR}" + local REF_VAR="${PROJECT}_CI_REF" + local REF="${!REF_VAR}" if [ -d "$DEST" ]; then echo "Warning: download and unpacking of $PROJECT skipped because $DEST already exists." elif [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then - local GITURL_VAR="${PROJECT}_CI_GITURL" - local GITURL="${!GITURL_VAR}" - local REF_VAR="${PROJECT}_CI_REF" - local REF="${!REF_VAR}" git clone "$GITURL" "$DEST" cd "$DEST" git checkout "$REF" else # When possible, we download tarballs to reduce bandwidth and latency local ARCHIVEURL_VAR="${PROJECT}_CI_ARCHIVEURL" local ARCHIVEURL="${!ARCHIVEURL_VAR}" - local REF_VAR="${PROJECT}_CI_REF" - local REF="${!REF_VAR}" mkdir -p "$DEST" cd "$DEST" - wget "$ARCHIVEURL/$REF.tar.gz" - tar xvfz "$REF.tar.gz" --strip-components=1 - rm -f "$REF.tar.gz" + local COMMIT=$(git ls-remote "$GITURL" "refs/heads/$REF" | cut -f 1) + if [[ "$COMMIT" == "" ]]; then + # $REF must have been a tag or hash, not a branch + COMMIT="$REF" + fi + wget "$ARCHIVEURL/$COMMIT.tar.gz" + tar xvfz "$COMMIT.tar.gz" --strip-components=1 + rm -f "$COMMIT.tar.gz" fi } |
