script for downloading components from central store
authorhaftmann
Sun, 29 Jul 2012 21:55:56 +0200
changeset 48593 c895e334162c
parent 48592 a125b8040ada
child 48594 c24907e5081e
child 48596 3defa60a7ae3
script for downloading components from central store
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