diff options
author | Karel Kočí <karel.koci@nic.cz> | 2018-08-27 13:49:37 +0200 |
---|---|---|
committer | Karel Kočí <karel.koci@nic.cz> | 2018-08-27 13:49:37 +0200 |
commit | 97bf9457b18156e77c5fb6e9d61fbcdc93e06163 (patch) | |
tree | 2cf727c3c227afad906e516eaf1c91a1ce28a3ae /scripts | |
parent | ce879bd8fe3ebab10b32cb08c2d0d4e8d750306c (diff) | |
download | laminar-cnf-97bf9457b18156e77c5fb6e9d61fbcdc93e06163.tar.gz laminar-cnf-97bf9457b18156e77c5fb6e9d61fbcdc93e06163.tar.bz2 laminar-cnf-97bf9457b18156e77c5fb6e9d61fbcdc93e06163.zip |
Change how we do git mirror
This is more resilient approach and we should use it instead of original
approach.
Diffstat (limited to 'scripts')
-rw-r--r-- | scripts/utils | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/scripts/utils b/scripts/utils index 388d399..c28a2ea 100644 --- a/scripts/utils +++ b/scripts/utils @@ -5,18 +5,25 @@ echo_stage() { echo "========== $@ ==========" } -# Fetch git repository to WORKSPACE and create workspace in current directory +# Fetch bare git repository to WORKSPACE +# First argument has to be a source URL +# Second argument is name of directory to which will be repository cloned to. +git_fetch_bare() { + if [ -d "$WORKSPACE/$2" ]; then + git --git-dir="$WORKSPACE/$2" --bare remote update + else + git clone --mirror "$1" "$WORKSPACE/$2" + fi +} + +# Calls git_fetch_bare and then creates detached work tree in run directory # First agument has to be a source URL # Second argument is name of directory to which will be directory cloned in. # Second argument is optional and should be branch name (master is used if not # provided). git_fetch() { + git_fetch_bare "$1" "$2" local BRANCH="$3" [ -n "$BRANCH" ] || BRANCH=master - if [ -d "$WORKSPACE/$2" ]; then - git --git-dir="$WORKSPACE/$2" --bare fetch --prune --prune-tags --force "$1" "$BRANCH:$BRANCH" - else - git clone --bare "$1" "$WORKSPACE/$2" - fi git --git-dir="$WORKSPACE/$2" --bare worktree add --detach $2 $BRANCH } |