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