From 97bf9457b18156e77c5fb6e9d61fbcdc93e06163 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Karel=20Ko=C4=8D=C3=AD?= <karel.koci@nic.cz>
Date: Mon, 27 Aug 2018 13:49:37 +0200
Subject: Change how we do git mirror

This is more resilient approach and we should use it instead of original
approach.
---
 scripts/utils | 19 +++++++++++++------
 1 file 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
 }
-- 
cgit v1.2.3