diff options
author | Maxim Kuvyrkov <maxim.kuvyrkov@linaro.org> | 2019-01-15 10:26:07 +0000 |
---|---|---|
committer | Maxim Kuvyrkov <maxim.kuvyrkov@linaro.org> | 2019-01-15 10:26:07 +0000 |
commit | abf4d3217a50d4432efb74d78f29cac64f185f55 (patch) | |
tree | 61cae247883e42f378f762a97e64d2c411db8dde | |
parent | 1ac7c43e38e67a54fb9436add2ed1734328c7e00 (diff) |
jenkins-helpers.sh: Workaround stale "git gc" lock.
If build times out during "git gc" or "git gc" is otherwise
killed, then we have to clean up a stale lock.
Change-Id: I2c60b0a35a0881c2b5b893f6f925ffab5f88fcd4
-rw-r--r-- | jenkins-helpers.sh | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/jenkins-helpers.sh b/jenkins-helpers.sh index 83f4aee4..cab20f21 100644 --- a/jenkins-helpers.sh +++ b/jenkins-helpers.sh @@ -382,7 +382,11 @@ clone_or_update_repo_no_checkout () else # Clean up the clone (this is supposed to re-share objects from # reference clone and keep the size of the clone minimal). - git -C "$dir" gc + # It's possible that previous GC process was interrupted and left + # a lock. Use --force to workaround that. It should be safe + # to override the lock since directories should not be shared + # between concurrent builds. + git -C "$dir" gc --force fi ( |