ci: retry the generated-docs push through a rebase on rejection #171
@@ -181,7 +181,25 @@ jobs:
|
||||
git add docs/fish-config.md docs/fish-config.1 conf.d/__fish_config_op_registry.fish
|
||||
git diff --cached --quiet && echo "No changes to commit" && exit 0
|
||||
git commit -m "chore(docs): regenerate manual, man page, and component registry"
|
||||
git push
|
||||
|
||||
# npm ci + astro build + the Cloudflare deploy above can take
|
||||
# several minutes, so main can move (another PR merges) before
|
||||
# this push lands -- a bare `git push` was seen rejected as
|
||||
# non-fast-forward for exactly that reason (run 976). This
|
||||
# commit only ever touches generated files, so a rebase onto
|
||||
# whatever landed is always mechanical; retry it a few times
|
||||
# against a live race instead of failing the whole job.
|
||||
pushed=0
|
||||
for attempt in 1 2 3; do
|
||||
if git push; then
|
||||
pushed=1
|
||||
break
|
||||
fi
|
||||
echo "push rejected (attempt $attempt/3), rebasing onto origin/main..." >&2
|
||||
git fetch origin main
|
||||
git rebase origin/main
|
||||
done
|
||||
test "$pushed" -eq 1
|
||||
|
||||
# Stand-in for the GitHub mirror so the commit gets a completed status
|
||||
# instead of the real jobs above sitting queued forever for a
|
||||
|
||||
Reference in New Issue
Block a user