diff options
| author |  Dirk Hohndel <dirk@hohndel.org> | 2019-01-09 08:08:59 -0800 |
|---|---|---|
| committer | Dirk Hohndel <dirk@hohndel.org> | 2019-01-22 13:05:03 +1300 |
| commit | 0bd75c8e9e4ff0f7fbce5da3e8929e7deaf5a723 (patch) | |
| tree | cac1ffaa3489602bb5d7dae7fede3bf0a6e767ff /scripts | |
| parent | ddac55a3f12bd11fc8b3c412c919d1d9312b3a9c (diff) | |
| download | subsurface-0bd75c8e9e4ff0f7fbce5da3e8929e7deaf5a723.tar.gz | |
build system: try harder to checkout the right version
And actually fail a build if that doesn't work.
Signed-off-by: Dirk Hohndel <dirk@hohndel.org>
Diffstat (limited to 'scripts')
| -rwxr-xr-x | scripts/get-dep-lib.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/scripts/get-dep-lib.sh b/scripts/get-dep-lib.sh index 15796ae80..ccda4bcb7 100755 --- a/scripts/get-dep-lib.sh +++ b/scripts/get-dep-lib.sh @@ -46,9 +46,9 @@ git_checkout_library() { if [ ! "$current_sha" = "$target_sha" ] ; then git fetch origin - if ! git checkout "$version" ; then + if ! git checkout -f "$version" ; then echo "Can't find the right tag in $name - giving up" - return 1 + exit 1 fi fi popd |