diff options
| author | Karel Kočí <cynerd@email.cz> | 2018-08-26 16:48:18 +0200 |
|---|---|---|
| committer | Karel Kočí <cynerd@email.cz> | 2018-08-26 16:48:18 +0200 |
| commit | 78483e0fdd6ccfbc4de04028d40d97a2f32bee49 (patch) | |
| tree | 928a34c44ecb04cf02e562c875a4efc4e9e9dc4c | |
| parent | 16ce36f5c70ad57aba52e8bc3af2d2e1c30fc292 (diff) | |
| download | laminar-cnf-78483e0fdd6ccfbc4de04028d40d97a2f32bee49.tar.gz laminar-cnf-78483e0fdd6ccfbc4de04028d40d97a2f32bee49.tar.bz2 laminar-cnf-78483e0fdd6ccfbc4de04028d40d97a2f32bee49.zip | |
Another try
| -rw-r--r-- | scripts/utils | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/scripts/utils b/scripts/utils index 58372c5..65ee41a 100644 --- a/scripts/utils +++ b/scripts/utils @@ -13,8 +13,8 @@ echo_stage() { git_fetch() { local BRANCH="$3" [ -n "$BRANCH" ] || BRANCH=master - local GITARGS="--git-dir='$WORKSPACE/$2' --bare" - if [ -d "$WORKSPACE/$2/.git" ]; then + local GITARGS="--git-dir=\"$WORKSPACE/$2\" --bare" + if [ -d "$WORKSPACE/$2" ]; then git $GITARGS fetch --prune --prune-tags --force "$1" "$BRANCH:$BRANCH" else git clone --bare "$1" "$WORKSPACE/$2" |