4
4
filename=${directory}.tar.gz
8
8
my_destdir=${MAUS_ROOT_DIR}/third_party
10
10
if [ -n "${MAUS_ROOT_DIR+x}" ]; then
14
15
echo "INFO: Found source archive in 'source' directory"
16
17
echo "INFO: Source archive doesn't exist. Downloading..."
18
19
wget ${url} -O "${MAUS_ROOT_DIR}/third_party/source/${filename}"
21
23
if [ -e "${MAUS_ROOT_DIR}/third_party/source/${filename}" ]