src/ci/docker/dist-various-2/shared.sh

   1 hide_output() {
   2   { set +x; } 2>/dev/null
   3   on_err="
   4 echo ERROR: An error was encountered with the build.
   5 cat /tmp/build.log
   6 exit 1
   7 "
   8   trap "$on_err" ERR
   9   bash -c "while true; do sleep 30; echo \$(date) - building ...; done" &
  10   PING_LOOP_PID=$!
  11   "$@" &> /tmp/build.log
  12   trap - ERR
  13   kill $PING_LOOP_PID
  14   set -x
  15 }
  16
  17 # Copied from ../../shared.sh
  18 function retry {
  19   echo "Attempting with retry:" "$@"
  20   local n=1
  21   local max=5
  22   while true; do
  23     "$@" && break || {
  24       if [[ $n -lt $max ]]; then
  25         sleep $n  # don't retry immediately
  26         ((n++))
  27         echo "Command failed. Attempt $n/$max:"
  28       else
  29         echo "The command has failed after $n attempts."
  30         return 1
  31       fi
  32     }
  33   done
  34 }
  35
  36 # Copied from ../../init_repo.sh
  37 function fetch_github_commit_archive {
  38     local module=$1
  39     local cached="download-${module//\//-}.tar.gz"
  40     retry sh -c "rm -f $cached && \
  41         curl -f -sSL -o $cached $2"
  42     mkdir $module
  43     touch "$module/.git"
  44     tar -C $module --strip-components=1 -xf $cached
  45     rm $cached
  46 }