diff options
Diffstat (limited to 'scripts/utils')
| -rw-r--r-- | scripts/utils | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/scripts/utils b/scripts/utils index c17e37f..e05f10d 100644 --- a/scripts/utils +++ b/scripts/utils @@ -25,12 +25,19 @@ echo_fail() { } ## GIT ########################################################################## +# Locked git +lgit() { + local gitdir="$1" + shift + flock --exclusive "$gitdir" git --git-dir="$gitdir" "$@" +} + # Fetch bare git repository # First argument has to be a source URL # Second argument is path to directory to which will be repository cloned to. git_fetch_bare() { if [ -d "$2" ]; then - git --git-dir="$2" --bare remote update --prune + lgit "$2" --bare remote update --prune else git clone --mirror "$1" "$2" fi @@ -42,8 +49,8 @@ _git_fetch() { local branch="$3" [ -n "$branch" ] || branch=master git_fetch_bare "$1" "$4/$2" - git --git-dir="$4/$2" --bare worktree prune # remove old work trees - git --git-dir="$4/$2" --bare worktree add --force --detach "$2" "$branch" + lgit "$4/$2" --bare worktree prune # remove old work trees + lgit "$4/$2" --bare worktree add --force --detach "$2" "$branch" } # Fetch git repository with mirror |