diff options
| author | Oliver Smith <osmith@sysmocom.de> | 2022-10-17 12:17:04 +0200 |
|---|---|---|
| committer | osmith <osmith@sysmocom.de> | 2022-10-20 14:44:36 +0000 |
| commit | 1259ab99c6fb97fd17095935b429985b6f6b9b76 (patch) | |
| tree | b74b85be4399720b1ec288d852750d5769e32437 /contrib | |
| parent | 8a66dcd1f8e2c0d08aa97095e706922dfc00d97c (diff) | |
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
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/jenkins.sh | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/contrib/jenkins.sh b/contrib/jenkins.sh index 6512af9..96becc7 100755 --- a/contrib/jenkins.sh +++ b/contrib/jenkins.sh @@ -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 |