diff options
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  } | 
