From 7923507e76e8d64c6c457664ec59f10c884a9fb0 Mon Sep 17 00:00:00 2001
From: Dirk Hohndel <dirk@hohndel.org>
Date: Wed, 9 Jan 2019 08:08:59 -0800
Subject: [PATCH] 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>
---
 scripts/get-dep-lib.sh | 4 ++--
 1 file 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