summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKarel Kočí <karel.koci@nic.cz>2018-08-27 13:49:37 +0200
committerKarel Kočí <karel.koci@nic.cz>2018-08-27 13:49:37 +0200
commit97bf9457b18156e77c5fb6e9d61fbcdc93e06163 (patch)
tree2cf727c3c227afad906e516eaf1c91a1ce28a3ae
parentce879bd8fe3ebab10b32cb08c2d0d4e8d750306c (diff)
downloadlaminar-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.
-rw-r--r--scripts/utils19
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
}