diff options
| author | Karel Kočí <cynerd@email.cz> | 2020-11-24 16:17:01 +0100 |
|---|---|---|
| committer | Karel Kočí <cynerd@email.cz> | 2020-11-24 16:17:01 +0100 |
| commit | a1d7dcb6d990343c3c689114531f2b49daa8bb04 (patch) | |
| tree | 711367ccd6e8ce41fb7732c2e3a0f8c2f060a570 /scripts/utils | |
| parent | 0c431b64884b0665e3165d69e7537203fca03793 (diff) | |
| download | laminar-cnf-a1d7dcb6d990343c3c689114531f2b49daa8bb04.tar.gz laminar-cnf-a1d7dcb6d990343c3c689114531f2b49daa8bb04.tar.bz2 laminar-cnf-a1d7dcb6d990343c3c689114531f2b49daa8bb04.zip | |
scripts/utils: try to lock when hacking worktree
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 |