From a7efcb729ed1044ce0c81a9ca0eab4ae454de323 Mon Sep 17 00:00:00 2001
From: Guy Shimko <guy.shimko@gmail.com>
Date: Wed, 15 Jan 2025 23:09:50 +0200
Subject: [PATCH] build: delete package dir before redownloading it
---
src/compilation/download_packages.sh | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/src/compilation/download_packages.sh b/src/compilation/download_packages.sh
index 585878e..ff630cb 100755
--- a/src/compilation/download_packages.sh
+++ b/src/compilation/download_packages.sh
@@ -103,6 +103,10 @@ function extract_package() {
popd > /dev/null
+ # Make sure output dir is empty, so we could move content into it.
+ # The directory might not exist, so we need to pass || true so that set -e won't fail us.
+ rm -rf "$output_dir" || true
+
mv "$temp_dir/$package_dir" "$output_dir"
if [[ $? -ne 0 ]]; then
return 1