Merge branch 'master' into feature/necsave.

This commit is contained in:
José Pinto 2016-02-11 14:27:09 +00:00
commit de84a56ab3

View File

@ -28,16 +28,15 @@ download_tool()
{ {
wget -c "$1" -O "$2" wget -c "$1" -O "$2"
if [ $? -eq 0 ]; then if [ $? -eq 0 ]; then
rm -f "$2"
return 0 return 0
fi fi
curl -f -C - "$1" -o "$2" curl -f -C - "$1" -o "$2"
if [ $? -eq 0 ]; then if [ $? -eq 0 ]; then
rm -f "$2"
return 0 return 0
fi fi
rm -f "$2"
return 1 return 1
} }