You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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 : )
The text was updated successfully, but these errors were encountered:
The only item remaining on the checklist for releases is:
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?)I'm opening this issue so that we don't forget : )
The text was updated successfully, but these errors were encountered: