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

[ admin ] Finish v0.7.0 docs, upload release tarball #3173

Open
2 tasks
CodingCellist opened this issue Dec 22, 2023 · 0 comments
Open
2 tasks

[ admin ] Finish v0.7.0 docs, upload release tarball #3173

CodingCellist opened this issue Dec 22, 2023 · 0 comments

Comments

@CodingCellist
Copy link
Collaborator

CodingCellist commented Dec 22, 2023

The only item remaining on the checklist for releases is:

  • Make libdocs and upload to idris-lang.org

I can make the docs without any issues. However, there was some confusion about which Idris2 website is the "correct" one; whether there's an administrative change going on between some of them; who needs to switch what; etc. So I'm not too sure where to submit the new docs...

Additionally, the mkdist.sh-script creates a tarball containing the latest release. Afaict, this needs uploading to the website as well, since various package managers use it as the source of truth for releases (although it might be better to ask them to move to the GH sources so that there isn't duplicated work?)

  • Sort out release tarball

I'm opening this issue so that we don't forget : )

@CodingCellist CodingCellist added this to the 0.7.0 milestone Dec 22, 2023
@CodingCellist CodingCellist changed the title [ admin ] Finish v0.7.0 docs [ admin ] Finish v0.7.0 docs, upload release tarball Dec 22, 2023
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

1 participant