jenkins: retry build_devel (#30628)

* will it work

* retry build devel

* correct p[ath

* try a failure

* Revert "try a failure"

This reverts commit ba4e6a0a2096b94887fcfbf7d011e34aa2a16c41.
old-commit-hash: 36bebb1aa064b4b40580aa48d35b21bd9ebe14c2

scripts/retry.sh

@@ -0,0 +1,27 @@
+#!/bin/bash
+
+function fail {
+  echo $1 >&2
+  exit 1
+}
+
+function retry {
+  local n=1
+  local max=3 # 3 retries before failure
+  local delay=5 # delay between retries, 5 seconds
+  while true; do
+    echo "Running command '$@' with retry, attempt $n/$max"
+    "$@" && break || {
+      if [[ $n -lt $max ]]; then
+        ((n++))
+        sleep $delay;
+      else
+        fail "The command has failed after $n attempts."
+      fi
+    }
+  done
+}
+
+if [[ "${BASH_SOURCE[0]}" == "${0}" ]]; then
+    retry "$@"
+fi