Skip to content

Conversation

@Ruben-VandeVelde
Copy link
Contributor

No description provided.

@PatrickMassot
Copy link
Member

Could you please explain the changes to scripts/build_docs.sh?

@grunweg
Copy link
Collaborator

grunweg commented Dec 13, 2025

Otherwise, LGTM - thanks for doing this!

@Ruben-VandeVelde
Copy link
Contributor Author

4.25.2 was a half-finished release - doc-gen didn't get the tag, so the script's approach of assuming every release will have a corresponding tag doesn't work.

@grunweg
Copy link
Collaborator

grunweg commented Dec 14, 2025

Makes sense. Since future PRs will revert this anyway, I'm fine with merging this. Thanks again!

@grunweg grunweg merged commit 4e31ae3 into leanprover-community:master Dec 14, 2025
1 check passed
@Ruben-VandeVelde Ruben-VandeVelde deleted the bump-25-2 branch December 15, 2025 12:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants