Admin/lib/Tools/makedist_bundle
changeset 63490 9416333a17c2
parent 63058 8804faa80bc9
child 63897 85c83757788c
--- a/Admin/lib/Tools/makedist_bundle	Thu Jul 14 11:34:18 2016 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Thu Jul 14 12:20:20 2016 +0200
@@ -113,9 +113,11 @@
                 echo "  component $COMPONENT"
                 CONTRIB="$ARCHIVE_DIR/contrib/${COMPONENT}.tar.gz"
                 if [ ! -f "$CONTRIB" ]; then
+                  type -p curl  > /dev/null || fail "Cannot download files: missing curl"
                   REMOTE="$ISABELLE_COMPONENT_REPOSITORY/${COMPONENT}.tar.gz"
-                  echo "  download $REMOTE"
-                  perl -MLWP::Simple -e "getprint '$REMOTE';" > "$CONTRIB"
+                  echo "  downloading $REMOTE"
+                  curl --fail --silent "$REMOTE" > "$CONTRIB" || \
+                    fail "Failed to download \"$REMOTE\""
                   perl -e "exit((stat('${CONTRIB}'))[7] == 0 ? 0 : 1);" && exit 2
                 fi