Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Deploy doc rendering for v2.1 #2452

Open
andreasabel opened this issue Aug 1, 2024 · 2 comments
Open

Deploy doc rendering for v2.1 #2452

andreasabel opened this issue Aug 1, 2024 · 2 comments

Comments

@andreasabel
Copy link
Member

From https://agda.zulipchat.com/#narrow/stream/259646-announce/topic/Standard.20library.20v2.2E1/near/455502043

When will https://agda.github.io/agda-stdlib/v2.1/ be available?

NB: Listing the docs under https://agda.github.io/agda-stdlib will probably remain a manual process, but pushing the docs to subfolder tag for a new tag tag could probably be done by CI.

@jamesmckinna
Copy link
Contributor

@gallais is this still a manual process, or already part of the CI workflow?

@gallais
Copy link
Member

gallais commented Aug 1, 2024

Manual (but documented in the release guide)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants