# HG changeset patch
# User wenzelm
# Date 1602239259 -7200
# Node ID da577e2d42b36318a98c53bc645b2a9bd734979d
# Parent  2daa5f549687c9f98225b12ce85c54d8bc9da830
clarified according to Isabelle_System.download;

diff -r 2daa5f549687 -r da577e2d42b3 lib/Tools/components
--- a/lib/Tools/components	Fri Oct 09 12:01:35 2020 +0200
+++ b/lib/Tools/components	Fri Oct 09 12:27:39 2020 +0200
@@ -127,7 +127,7 @@
         type -p curl > /dev/null || fail "Cannot download files: missing curl"
         echo "Getting \"$REMOTE\""
         mkdir -p "$(dirname "$FULL_NAME")"
-        curl --fail --silent "$REMOTE" > "${FULL_NAME}.tar.gz.part" || \
+        curl --fail --silent --location "$REMOTE" > "${FULL_NAME}.tar.gz.part" || \
           fail "Failed to download \"$REMOTE\""
         if perl -e "exit((stat('${FULL_NAME}.tar.gz.part'))[7] == 0 ? 0 : 1);"
         then