Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more robust;
authorwenzelm
Tue, 09 Mar 2021 18:52:24 +0100
changeset 73402 7eecb5231f61
parent 73401 8b464825d2b5
child 73403 e19cb4c11409
more robust; eliminated perl;
lib/Tools/components file | annotate | diff | comparison | revisions 
--- a/lib/Tools/components	Tue Mar 09 18:44:43 2021 +0100
+++ b/lib/Tools/components	Tue Mar 09 18:52:24 2021 +0100
@@ -145,13 +145,12 @@
         type -p curl > /dev/null || fail "Cannot download files: missing curl"
         echo "Getting \"$REMOTE\""
         mkdir -p "$(dirname "$FULL_NAME")"
-        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);"
+        if curl --fail --silent --location "$REMOTE" > "${FULL_NAME}.tar.gz.part"
         then
-          rm -f "${FULL_NAME}.tar.gz.part"
+          mv -f "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz"
         else
-          mv "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz"
+          rm -f "${FULL_NAME}.tar.gz.part"
+          fail "Failed to download \"$REMOTE\""
         fi
       fi
       if [ -e "${FULL_NAME}.tar.gz" ]; then
isabelle