|
@@ -47,13 +47,15 @@ git_cache="${dl_dir}/git"
|
|
# fetch'ed later.
|
|
# fetch'ed later.
|
|
if [ ! -d "${git_cache}" ]; then
|
|
if [ ! -d "${git_cache}" ]; then
|
|
_git init "'${git_cache}'"
|
|
_git init "'${git_cache}'"
|
|
- pushd "${git_cache}" >/dev/null
|
|
|
|
- _git remote add origin "'${uri}'"
|
|
|
|
- popd >/dev/null
|
|
|
|
fi
|
|
fi
|
|
|
|
|
|
pushd "${git_cache}" >/dev/null
|
|
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}'"
|
|
_git remote set-url origin "'${uri}'"
|
|
|
|
|
|
# Try to fetch with limited depth, since it is faster than a full clone - but
|
|
# Try to fetch with limited depth, since it is faster than a full clone - but
|