contrib/jenkins.sh: set-url for existing clones

Make sure that the recent change from git.osmocom.org ->
gerrit.osmocom.org for git clone urls is applied to the existing clones
as well.

Change-Id: I3d9c193bf353ecff0ee8bb4c507de59139fc0925
This commit is contained in:
Oliver Smith 2022-10-17 12:17:04 +02:00 committed by osmith
parent 8a66dcd1f8
commit 1259ab99c6
1 changed files with 12 additions and 1 deletions

View File

@ -5,7 +5,18 @@ WORKSPACE_DIR="$(realpath "$(dirname "$0")/..")"
# Clone repository to ~/, or update existing
# $1: name of osmocom project
clone_repo() {
cd ~/"$1" || (cd ~/ && git clone https://gerrit.osmocom.org/"$1" && cd ~/"$1")
local project="$1"
local url="https://gerrit.osmocom.org/$project"
if [ -d ~/"$project" ]; then
cd ~/"$project"
git remote set-url origin "$url"
else
cd ~
git clone "$url"
cd "$project"
fi
git rev-parse HEAD
git status