Skip to content

Commit

Permalink
Add diagnostics to help identify network problems
Browse files Browse the repository at this point in the history
  • Loading branch information
mernst committed Feb 5, 2020
1 parent 5ac3a66 commit 1980e05
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion init.sh
Expand Up @@ -49,12 +49,14 @@ fi
# remote resource is newer. Works around connections that hang. Takes a
# single command-line argument, a URL.
download_url() {
BASENAME=`basename ${@: -1}`
echo "Downloading $@"
if [ "$(uname)" = "Darwin" ] ; then
wget -nv -N "$@"
else
BASENAME=`basename ${@: -1}`
timeout 300 curl -s -S -R -L -O -z "$BASENAME" "$@" || (echo "retrying curl $@" && rm -f "$BASENAME" && curl -R -L -O -z "$BASENAME" "$@")
fi
echo "Downloaded $@"
}

# Get time of last data modification of a file
Expand Down

0 comments on commit 1980e05

Please sign in to comment.