File tree Expand file tree Collapse file tree 1 file changed +23
-1
lines changed Expand file tree Collapse file tree 1 file changed +23
-1
lines changed Original file line number Diff line number Diff line change @@ -308,7 +308,29 @@ runs:
308308 test ! -f "${BRANCH}/report.html" || git add "${BRANCH}/report.html"
309309 if [[ -n "$(git status --porcelain)" ]]; then
310310 git commit -m "update"
311- git push origin HEAD:coverage
311+
312+ max_attempts=5
313+ attempt=1
314+ while true; do
315+ if git push origin HEAD:coverage; then
316+ break
317+ fi
318+
319+ if (( attempt >= max_attempts )); then
320+ echo "Failed to push coverage branch after ${max_attempts} attempts." >&2
321+ exit 1
322+ fi
323+
324+ echo "Push rejected (attempt ${attempt}/${max_attempts}). Refreshing coverage branch..."
325+ git fetch origin coverage
326+ if ! git rebase origin/coverage; then
327+ echo "Rebase failed while updating coverage branch." >&2
328+ git rebase --abort || true
329+ exit 1
330+ fi
331+
332+ attempt=$(( attempt + 1 ))
333+ done
312334 else
313335 echo "No changes to commit."
314336 fi
You can’t perform that action at this time.
0 commit comments