4bee7629ee
Maintaining the download helpers in the Makefile has proved to be a bit complex, so move it to a shell script. Signed-off-by: "Yann E. MORIN" <yann.morin.1998@free.fr> Reviewed-by: Samuel Martin <s.martin49@gmail.com> Signed-off-by: Peter Korsgaard <peter@korsgaard.com>
22 lines
374 B
Bash
Executable File
22 lines
374 B
Bash
Executable File
#!/bin/bash
|
|
|
|
# We want to catch any command failure, and exit immediately
|
|
set -e
|
|
|
|
# Download helper for wget
|
|
# Call it with:
|
|
# $1: URL
|
|
# $2: output file
|
|
# And this environment:
|
|
# WGET : the wget command to call
|
|
|
|
url="${1}"
|
|
output="${2}"
|
|
|
|
if ${WGET} -O "${output}.tmp" "${url}"; then
|
|
mv "${output}.tmp" "${output}"
|
|
else
|
|
rm -f "${output}.tmp"
|
|
exit 1
|
|
fi
|