Maintaining the download helpers in the Makefile has proved to be a bit
complex, so move it to a shell script.
[Peter: redirect pushd/popd output to /dev/null]
Signed-off-by: "Yann E. MORIN" <yann.morin.1998@free.fr>
Reviewed-by: Samuel Martin <s.martin49@gmail.com>
Reviewed-by: Ryan Barnett <ryan.barnett@rockwellcollins.com>
Signed-off-by: Peter Korsgaard <peter@korsgaard.com>
