Skip to content
Snippets Groups Projects
Commit 3a48467d authored by Dan Guest's avatar Dan Guest
Browse files

Simpler way to ensure that externals points to the right URL

parent ae2739fe
No related branches found
No related tags found
No related merge requests found
...@@ -106,20 +106,11 @@ if [ ! -d "${SOURCEDIR}" ]; then ...@@ -106,20 +106,11 @@ if [ ! -d "${SOURCEDIR}" ]; then
_retry_ git clone ${EXTERNALSURL} ${SOURCEDIR} _retry_ git clone ${EXTERNALSURL} ${SOURCEDIR}
else else
echo "${SOURCEDIR} already exists -> assume previous checkout" echo "${SOURCEDIR} already exists -> assume previous checkout"
fi # make sure it points to the right place
(
# check whether the source directory points to the right repository cd ${SOURCEDIR}
RECLONE=false git remote set-url origin ${EXTERNALSURL}
pushd ${SOURCEDIR} )
SOURCEURL=$(git remote get-url origin)
if [ "${SOURCEURL}" != "${EXTERNALSURL}" ] ; then
echo "${SOURCEURL} wasn't cloned from ${EXTERNALSURL}, deleting"
RECLONE=true
fi
popd
if [ $RECLONE = true ] ; then
rm -rf ${SOURCEDIR}
_retry_ git clone ${EXTERNALSURL} ${SOURCEDIR}
fi fi
# Get the appropriate version of it: # Get the appropriate version of it:
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment