Skip to content

Prepare github actions tasks for deploying multiple documentation versions at once #12784

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

Closed

Conversation

BarkingBad
Copy link
Contributor

This PR is still in draft since it has some hardcoded since I was testing it manually locally. However, if you add another commit updating docs.csv with 2a621da (or any other commit hash/tag/branch) that has this changes already implemented and run ./project/scripts/genDocs you can publish docs correctly for multiple sources.

@ckipp01
Copy link
Member

ckipp01 commented May 10, 2023

I'm not sure who the doc guru is, @julienrf or @Kordyjan , but is this still relevant or can we close this?

@BarkingBad
Copy link
Contributor Author

It’s no longer relevant indeed

@BarkingBad BarkingBad closed this May 10, 2023
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.

dotty.epfl.ch/docs should provide option to pick up a version that is documented
3 participants