From ff1a7a81a77f0b673e58d7ba4317a4c41311115d Mon Sep 17 00:00:00 2001
From: Justin Newberry <justin@comma.ai>
Date: Wed, 6 Dec 2023 15:37:36 -0800
Subject: [PATCH] will it work

---
 release/build_devel.sh |  7 +++++--
 scripts/retry.sh       | 23 +++++++++++++++++++++++
 2 files changed, 28 insertions(+), 2 deletions(-)
 create mode 100755 scripts/retry.sh

diff --git a/release/build_devel.sh b/release/build_devel.sh
index ca04c56f1e..62496d7fec 100755
--- a/release/build_devel.sh
+++ b/release/build_devel.sh
@@ -22,8 +22,11 @@ pre-commit uninstall || true
 
 echo "[-] bringing master-ci and devel in sync T=$SECONDS"
 cd $TARGET_DIR
-git fetch --depth 1 origin master-ci
-git fetch --depth 1 origin devel
+
+source scripts/retry.sh
+
+retry git fetch --depth 1 origin master-ci
+retry git fetch --depth 1 origin devel
 
 git checkout -f --track origin/master-ci
 git reset --hard master-ci
diff --git a/scripts/retry.sh b/scripts/retry.sh
new file mode 100755
index 0000000000..9d62ba1cba
--- /dev/null
+++ b/scripts/retry.sh
@@ -0,0 +1,23 @@
+#!/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
+}
\ No newline at end of file