3 { set +x; } 2>/dev/null
5 echo ERROR: An error was encountered with the build.
10 bash -c "while true; do sleep 30; echo \$(date) - building ...; done" &
12 "$@" &> /tmp/build.log
18 # Copied from ../../shared.sh
20 echo "Attempting with retry:" "$@"
25 if [[ $n -lt $max ]]; then
26 sleep $n # don't retry immediately
28 echo "Command failed. Attempt $n/$max:"
30 echo "The command has failed after $n attempts."
37 # Copied from ../../init_repo.sh
38 function fetch_github_commit_archive {
40 local cached="download-${module//\//-}.tar.gz"
41 retry sh -c "rm -f $cached && \
42 curl -f -sSL -o $cached $2"
45 tar -C $module --strip-components=1 -xf $cached