# HG changeset patch
# User haftmann
# Date 1343591756 -7200
# Node ID c895e334162ce06b9a6cbad35ad4c8cdfebb57df
# Parent  a125b8040ada37a96cf11f304dca9e9f408e6c30
script for downloading components from central store

diff -r a125b8040ada -r c895e334162c Admin/download-components
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/download-components	Sun Jul 29 21:55:56 2012 +0200
@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+#
+# Author: Florian Haftmann
+#
+# DESCRIPTION: Download and unpack components from central component store
+
+shopt -s -o errexit
+shopt -s -o nounset
+
+THIS="$(basename "$0")"
+HERE="$(cd $(dirname "$0"); cd "$(pwd -P)"; pwd)"
+
+trap 'echo "Error in ${THIS}" >&2' ERR
+
+function fail {
+  echo "$1" >&2
+  exit 1
+}
+
+ISABELLE_HOME_USER="$(isabelle getenv -b ISABELLE_HOME_USER)"
+: ${TMP:='/tmp'}
+REMOTE='http://isabelle.in.tum.de/components'
+LOCAL="${ISABELLE_HOME_USER}/contrib"
+SUFFIX='.tar.gz'
+
+for COMPONENT in "$@"
+do
+  COMPONENT_ARCHIVE="${COMPONENT}.tar.gz"
+  wget -nd --directory-prefix="${TMP}" "${REMOTE}/${COMPONENT_ARCHIVE}"
+  tar -xzv -f "${TMP}/${COMPONENT_ARCHIVE}" -C "${LOCAL}"
+  rm "${TMP}/${COMPONENT_ARCHIVE}"
+  echo
+done