From 27441486820190230ebd6216ae0edf6e98e35fa3 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 10:41:32 +0100 Subject: [PATCH 1/2] metrics: rebase-and-retry the commit-back push The metrics run takes several minutes; if master advances meanwhile (e.g. a PR is merged), the bot's push is rejected with 'fetch first'. Rebase onto origin/master and retry the push a few times. --- .github/workflows/metrics.yml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/.github/workflows/metrics.yml b/.github/workflows/metrics.yml index d3f0b5f..df519af 100644 --- a/.github/workflows/metrics.yml +++ b/.github/workflows/metrics.yml @@ -72,4 +72,12 @@ jobs: # Pushing with the default GITHUB_TOKEN does not retrigger workflows; # [skip ci] is belt-and-suspenders. No-op stays green. git commit -m "chore: update AFP metrics [skip ci]" || { echo "no changes"; exit 0; } - git push + # master may have advanced during the (multi-minute) run, which would + # reject the push; rebase onto the latest and retry a few times. + for attempt in 1 2 3 4 5; do + if git push; then exit 0; fi + echo "push rejected (attempt $attempt) - rebasing on origin/master ..." + git pull --rebase --autostash origin master + done + echo "failed to push metrics after retries" >&2 + exit 1 From ca27cdef8c24ffd5db07a453ca964c0731419962 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 10:41:57 +0100 Subject: [PATCH 2/2] ci: trigger