diff options
| -rwxr-xr-x | scripts/get-dep-lib.sh | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/scripts/get-dep-lib.sh b/scripts/get-dep-lib.sh index bc76204f8..3fbfcd3c1 100755 --- a/scripts/get-dep-lib.sh +++ b/scripts/get-dep-lib.sh @@ -67,6 +67,9 @@ curl_download_library() { if [ ! -f "$filename" ]; then ${CURL} "${base_url}${filename}" + fi + + if [ ! -d "$name" ] || [ "$name" -ot "$filename" ] ; then rm -rf "$name" mkdir "$name" tar -C "$name" --strip-components=1 -xf "$filename" |