diff options
| -rwxr-xr-x | support/download/git | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/support/download/git b/support/download/git index 868dfad0dd..381f3ceeb3 100755 --- a/support/download/git +++ b/support/download/git @@ -47,13 +47,15 @@ git_cache="${dl_dir}/git" # fetch'ed later. if [ ! -d "${git_cache}" ]; then _git init "'${git_cache}'" - pushd "${git_cache}" >/dev/null - _git remote add origin "'${uri}'" - popd >/dev/null fi pushd "${git_cache}" >/dev/null +# Ensure the repo has an origin (in case a previous run was killed). +if ! git remote |grep -q -E '^origin$'; then + _git remote add origin "'${uri}'" +fi + _git remote set-url origin "'${uri}'" # Try to fetch with limited depth, since it is faster than a full clone - but |
