diff --git a/tools/grab_file b/tools/grab_file new file mode 100755 index 00000000..24b260ca --- /dev/null +++ b/tools/grab_file @@ -0,0 +1,32 @@ +#!/bin/sh +# +# grab_file +# +# extra utility script - if a file does not exist in our mirror and +# we've been told to use an http mirror, go grab it from there +# +# Takes 1 parameters: the the full path to the file (relative to the +# base dir of the mirror) +# +# The MIRROR env var must be set +# If we want to be able to download, HTTPMIRROR mus be set too + +set -e +#set -x + +WANTED=$1 + +if [ "$MIRROR"x = ""x ] ; then + echo $0: MIRROR not set + exit 1 +fi + +if [ -e "$MIRROR/$WANTED" ] ; then + exit 0 +fi + +# else + +DIR=$(dirname "$WANTED") +mkdir -p "$MIRROR/$DIR" +wget -o /tmp/log -q "$HTTPMIRROR/$WANTED" -O "$MIRROR/$WANTED"