1 files changed, 35 insertions, 0 deletions
diff --git a/src/ci/docker/host-x86_64/dist-various-2/shared.sh b/src/ci/docker/host-x86_64/dist-various-2/shared.sh
new file mode 100644
index 000000000..291f26bda
--- /dev/null
+++ b/src/ci/docker/host-x86_64/dist-various-2/shared.sh
@@ -0,0 +1,35 @@
+#!/usr/bin/env bash
+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
+}
+
+# Copied from ../../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
+}