Fix libs/setup.sh nocached download (#148)

This commit is contained in:
Marko Budiselić 2021-05-13 12:05:36 +02:00 committed by GitHub
parent 782c377f5d
commit 1def0c9104
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -16,7 +16,11 @@ clone () {
shift 3
# Clone if there's no repo.
if [[ ! -d "$dir_name" ]]; then
git clone "$git_repo" "$dir_name"
echo "Cloning from $git_repo"
# If the clone fails, it doesn't make sense to continue with the function
# execution but the whole script should continue executing because we might
# clone the same repo from a different source.
git clone "$git_repo" "$dir_name" || return 1
fi
pushd "$dir_name"
# Just fetch new commits from remote repository. Don't merge/pull them in, so