more uniform options for "curl", following lib/Tools/components;
authorwenzelm
Mon, 23 Jan 2023 14:26:42 +0100
changeset 77052 86ace3c45837
parent 77051 e57ba228ec24
child 77053 c839b84ee66f
more uniform options for "curl", following lib/Tools/components;
Admin/Windows/Cygwin/setup_server
src/Pure/Tools/build_docker.scala
--- 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"
--- 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 && \