Skip to content

Conversation

@giordano
Copy link
Contributor

@giordano giordano commented Nov 7, 2025

git push --force is really a bad practice, git push --force-with-lease prevents issues in case of race conditions. Of course this can cause some deployments to fail and arguably users should orchestrate the docs publishing jobs to avoid conflicts (e.g. using concurrency groups), but I think it's better for a git push to fail loudly rather than catastrophically and silently erase data if all other barriers fail.

Copy link
Collaborator

@fingolfin fingolfin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sounds like a good idea to me, but we need a CHANGELOG entry, given that this could cause breakage for people (a good kind of breakage, but they'll wonder what changed to cause it, so we should list it).

Could you please add one?

@fingolfin fingolfin merged commit 6bdbcc4 into JuliaDocs:master Nov 7, 2025
26 of 27 checks passed
@giordano giordano deleted the patch-2 branch November 7, 2025 15:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants