prefer curl: presumably more portable and versatile;
authorwenzelm
Thu Jul 14 12:20:20 2016 +0200 (2016-07-14)
changeset 634909416333a17c2
parent 63489 cd540c8031a4
child 63491 58ccbc73a172
prefer curl: presumably more portable and versatile;
Admin/lib/Tools/makedist_bundle
Admin/lib/Tools/makedist_cygwin
README_REPOSITORY
lib/Tools/components
     1.1 --- a/Admin/lib/Tools/makedist_bundle	Thu Jul 14 11:34:18 2016 +0200
     1.2 +++ b/Admin/lib/Tools/makedist_bundle	Thu Jul 14 12:20:20 2016 +0200
     1.3 @@ -113,9 +113,11 @@
     1.4                  echo "  component $COMPONENT"
     1.5                  CONTRIB="$ARCHIVE_DIR/contrib/${COMPONENT}.tar.gz"
     1.6                  if [ ! -f "$CONTRIB" ]; then
     1.7 +                  type -p curl  > /dev/null || fail "Cannot download files: missing curl"
     1.8                    REMOTE="$ISABELLE_COMPONENT_REPOSITORY/${COMPONENT}.tar.gz"
     1.9 -                  echo "  download $REMOTE"
    1.10 -                  perl -MLWP::Simple -e "getprint '$REMOTE';" > "$CONTRIB"
    1.11 +                  echo "  downloading $REMOTE"
    1.12 +                  curl --fail --silent "$REMOTE" > "$CONTRIB" || \
    1.13 +                    fail "Failed to download \"$REMOTE\""
    1.14                    perl -e "exit((stat('${CONTRIB}'))[7] == 0 ? 0 : 1);" && exit 2
    1.15                  fi
    1.16  
     2.1 --- a/Admin/lib/Tools/makedist_cygwin	Thu Jul 14 11:34:18 2016 +0200
     2.2 +++ b/Admin/lib/Tools/makedist_cygwin	Thu Jul 14 12:20:20 2016 +0200
     2.3 @@ -43,7 +43,9 @@
     2.4  [ ! -e "$TARGET" ] || fail "Target already exists: \"$TARGET\""
     2.5  mkdir -p "$TARGET/isabelle" || fail "Failed to create target directory: \"$TARGET\""
     2.6  
     2.7 -perl -MLWP::Simple -e "getprint '$CYGWIN_MIRROR/setup-x86.exe';" > "$TARGET/isabelle/cygwin.exe"
     2.8 +type -p curl > /dev/null || fail "Cannot download files: missing curl"
     2.9 +curl --fail --silent "$CYGWIN_MIRROR/setup-x86.exe" > "$TARGET/isabelle/cygwin.exe" || \
    2.10 +  fail "Failed to download \"$CYGWIN_MIRROR/setup-x86.exe\""
    2.11  chmod +x "$TARGET/isabelle/cygwin.exe"
    2.12  
    2.13  "$TARGET/isabelle/cygwin.exe" -h </dev/null >/dev/null || exit 2
    2.14 @@ -55,7 +57,7 @@
    2.15    --site "$CYGWIN_MIRROR" --no-verify \
    2.16    --local-package-dir 'C:\temp' \
    2.17    --root "$(cygpath -w "$TARGET")" \
    2.18 -  --packages perl,perl-libwww-perl,rlwrap,unzip,nano \
    2.19 +  --packages curl,nano,perl,perl-libwww-perl,rlwrap,unzip \
    2.20    --no-shortcuts --no-startmenu --no-desktop --quiet-mode
    2.21  
    2.22  [ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2
     3.1 --- a/README_REPOSITORY	Thu Jul 14 11:34:18 2016 +0200
     3.2 +++ b/README_REPOSITORY	Thu Jul 14 12:20:20 2016 +0200
     3.3 @@ -4,11 +4,11 @@
     3.4  Quick start in 30min
     3.5  --------------------
     3.6  
     3.7 -1a. Linux and Mac OS X: ensure that Perl (with libwww) and Mercurial (hg)
     3.8 -    is installed (see also http://www.selenic.com/mercurial)
     3.9 +1a. Linux and Mac OS X: ensure that Mercurial is installed
    3.10 +    (see also http://www.selenic.com/mercurial)
    3.11  
    3.12 -1b. Windows: ensure that Cygwin with Perl and Mercurial is installed (see
    3.13 -    also http://www.cygwin.com)
    3.14 +1b. Windows: ensure that Cygwin with curl and Mercurial is installed
    3.15 +    (see also http://www.cygwin.com)
    3.16  
    3.17  2. Clone repository (bash shell commands):
    3.18  
     4.1 --- a/lib/Tools/components	Thu Jul 14 11:34:18 2016 +0200
     4.2 +++ b/lib/Tools/components	Thu Jul 14 12:20:20 2016 +0200
     4.3 @@ -124,9 +124,11 @@
     4.4      else
     4.5        if [ ! -e "${FULL_NAME}.tar.gz" ]; then
     4.6          REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
     4.7 +        type -p curl > /dev/null || fail "Cannot download files: missing curl"
     4.8          echo "Getting \"$REMOTE\""
     4.9          mkdir -p "$(dirname "$FULL_NAME")"
    4.10 -        perl -MLWP::Simple -e "getprint '$REMOTE';" > "${FULL_NAME}.tar.gz"
    4.11 +        curl --fail --silent "$REMOTE" > "${FULL_NAME}.tar.gz" || \
    4.12 +          fail "Failed to download \"$REMOTE\""
    4.13          if perl -e "exit((stat('${FULL_NAME}.tar.gz'))[7] == 0 ? 0 : 1);"
    4.14          then
    4.15            rm -f "${FULL_NAME}.tar.gz"