# HG changeset patch
# User wenzelm
# Date 1674480402 -3600
# Node ID 86ace3c4583788157c5c09be471733b39d992d6e
# Parent  e57ba228ec2445cbd49e1afbcb2de7e16a7a5d54
more uniform options for "curl", following lib/Tools/components;

diff -r e57ba228ec24 -r 86ace3c45837 Admin/Windows/Cygwin/setup_server
--- a/Admin/Windows/Cygwin/setup_server	Mon Jan 23 11:31:18 2023 +0100
+++ b/Admin/Windows/Cygwin/setup_server	Mon Jan 23 14:26:42 2023 +0100
@@ -15,7 +15,7 @@
   local DIR="${2:-.}"
   mkdir -p "$DIR" || fail "Cannot create directory: \"$DIR\""
   echo "Downloading $URL ..."
-  curl --fail --silent "$URL" > "$DIR"/"$(basename "$URL")" || fail "FAILED"
+  curl --fail --silent --location "$URL" > "$DIR"/"$(basename "$URL")" || fail "FAILED"
 }
 
 download "$CYGWIN_MAIN/setup-x86_64.exe"
diff -r e57ba228ec24 -r 86ace3c45837 src/Pure/Tools/build_docker.scala
--- a/src/Pure/Tools/build_docker.scala	Mon Jan 23 11:31:18 2023 +0100
+++ b/src/Pure/Tools/build_docker.scala	Mon Jan 23 14:26:42 2023 +0100
@@ -68,7 +68,7 @@
 # Isabelle
 WORKDIR /home/isabelle
 """ + (if (is_remote)
-       "RUN curl --fail --silent " + Bash.string(app_archive) + " > Isabelle.tar.gz"
+       "RUN curl --fail --silent --location " + Bash.string(app_archive) + " > Isabelle.tar.gz"
       else "COPY Isabelle.tar.gz .") + """
 RUN tar xzf Isabelle.tar.gz && \
   mv """ + isabelle_name + """ Isabelle && \