1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/download-components	Sun Jul 29 21:55:56 2012 +0200
     1.3 @@ -0,0 +1,33 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# Author: Florian Haftmann
     1.7 +#
     1.8 +# DESCRIPTION: Download and unpack components from central component store
     1.9 +
    1.10 +shopt -s -o errexit
    1.11 +shopt -s -o nounset
    1.12 +
    1.13 +THIS="$(basename "$0")"
    1.14 +HERE="$(cd $(dirname "$0"); cd "$(pwd -P)"; pwd)"
    1.15 +
    1.16 +trap 'echo "Error in ${THIS}" >&2' ERR
    1.17 +
    1.18 +function fail {
    1.19 +  echo "$1" >&2
    1.20 +  exit 1
    1.21 +}
    1.22 +
    1.23 +ISABELLE_HOME_USER="$(isabelle getenv -b ISABELLE_HOME_USER)"
    1.24 +: ${TMP:='/tmp'}
    1.25 +REMOTE='http://isabelle.in.tum.de/components'
    1.26 +LOCAL="${ISABELLE_HOME_USER}/contrib"
    1.27 +SUFFIX='.tar.gz'
    1.28 +
    1.29 +for COMPONENT in "$@"
    1.30 +do
    1.31 +  COMPONENT_ARCHIVE="${COMPONENT}.tar.gz"
    1.32 +  wget -nd --directory-prefix="${TMP}" "${REMOTE}/${COMPONENT_ARCHIVE}"
    1.33 +  tar -xzv -f "${TMP}/${COMPONENT_ARCHIVE}" -C "${LOCAL}"
    1.34 +  rm "${TMP}/${COMPONENT_ARCHIVE}"
    1.35 +  echo
    1.36 +done