Merge from rustc

1 files changed, 42 insertions, 0 deletions

diff --git a/src/ci/docker/scripts/shared.sh b/src/ci/docker/scripts/shared.sh
new file mode 100644
index 00000000000..9969659088d
--- /dev/null
+++ b/src/ci/docker/scripts/shared.sh
@@ -0,0 +1,42 @@
+#!/bin/false
+# shellcheck shell=bash
+
+# This file is intended to be sourced with `. shared.sh` or
+# `source shared.sh`, hence the invalid shebang and not being
+# marked as an executable file in git.
+
+function hide_output {
+  { set +x; } 2>/dev/null
+  on_err="
+echo ERROR: An error was encountered with the build.
+cat /tmp/build.log
+exit 1
+"
+  trap "$on_err" ERR
+  bash -c "while true; do sleep 30; echo \$(date) - building ...; done" &
+  PING_LOOP_PID=$!
+  "$@" &> /tmp/build.log
+  trap - ERR
+  kill $PING_LOOP_PID
+  set -x
+}
+
+# See https://unix.stackexchange.com/questions/82598
+# Duplicated in src/ci/shared.sh
+function retry {
+  echo "Attempting with retry:" "$@"
+  local n=1
+  local max=5
+  while true; do
+    "$@" && break || {
+      if [[ $n -lt $max ]]; then
+        sleep $n  # don't retry immediately
+        ((n++))
+        echo "Command failed. Attempt $n/$max:"
+      else
+        echo "The command has failed after $n attempts."
+        return 1
+      fi
+    }
+  done
+}