From bab90d483754aa9152a9f0c79f59261130ac2e5e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Josef=20S=C3=B6ntgen?= Date: Tue, 9 May 2023 13:34:10 +0200 Subject: [PATCH] depot/download: let curl fail on 404 response Downloading non-existent archives from 'depot.genode.org' leads to files in the 'public' directory containing the 404 error website delivered by the HTTP server. Specifying the '--fail' option results in curl generating an exit-code that leads to the appropriate action by the tool, e.g.: Error: failed to download 'https://depot.genode.org/user/pkg/x/version.tar.xz' Issue #4865. --- tool/depot/mk/downloader | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tool/depot/mk/downloader b/tool/depot/mk/downloader index 5051c5e903..48daaa95fd 100755 --- a/tool/depot/mk/downloader +++ b/tool/depot/mk/downloader @@ -110,7 +110,7 @@ file_url = '${URL($(call archive_user,$1))}/$1' $(PUBLIC_DIR)/%: @$(ECHO) "$(DARK_COL)download$(DEFAULT_COL) $*" $(VERBOSE)mkdir -p $(dir $@) - $(VERBOSE)curl --silent $(call file_url,$*) -o $@ ||\ + $(VERBOSE)curl --fail --silent $(call file_url,$*) -o $@ ||\ (echo "Error: failed to download $(call file_url,$*)"; rm -f $@; false) $(MAKECMDGOALS): $(TARGETS)