diff options
| -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 } |