diff options
author | Murillo Bernardes <mfbernardes@gmail.com> | 2018-06-16 18:27:35 +0200 |
---|---|---|
committer | Dirk Hohndel <dirk@hohndel.org> | 2018-06-17 08:25:59 +0900 |
commit | 7d92f5f8115b53fdca918f847d863ef3701976d1 (patch) | |
tree | ce5e751168f191bccbcc24263e4369e7e8e143a2 /scripts | |
parent | 550b6f179f10169eb674a5150e7ba357220d3c7a (diff) | |
download | subsurface-7d92f5f8115b53fdca918f847d863ef3701976d1.tar.gz |
build-system: avoid checkout when unneeded
Checkout only if current checked out version differs from
expected.
Signed-off-by: Murillo Bernardes <mfbernardes@gmail.com>
Diffstat (limited to 'scripts')
-rwxr-xr-x | scripts/get-dep-lib.sh | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/scripts/get-dep-lib.sh b/scripts/get-dep-lib.sh index c951ec813..970569c6c 100755 --- a/scripts/get-dep-lib.sh +++ b/scripts/get-dep-lib.sh @@ -38,10 +38,15 @@ git_checkout_library() { fi pushd "$name" - git fetch origin - if ! git checkout "$version" ; then - echo "Can't find the right tag in $name - giving up" - return -1 + local current_sha=$(git rev-parse HEAD) + local target_sha=$(git rev-parse "$version") + + if [ ! "$current_sha" = "$target_sha" ] ; then + git fetch origin + if ! git checkout "$version" ; then + echo "Can't find the right tag in $name - giving up" + return -1 + fi fi popd } |