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

ci: Build and push docs to Github Pages #10

Open
langston-barrett opened this issue Nov 14, 2023 · 1 comment
Open

ci: Build and push docs to Github Pages #10

langston-barrett opened this issue Nov 14, 2023 · 1 comment
Labels
CI Continuous integration

Comments

@langston-barrett
Copy link
Collaborator

Rather than ask interested parties to build the documentation themselves, we could build it in CI and host in on Github pages. See this build for an example. This should be done after open-sourcing, as the Github pages are public by default. This will require a repo administrator to enable Github Pages in the repo settings.

@kquick
Copy link
Member

kquick commented Nov 14, 2023

FYI, a more complicated CI process that allows for publishing multiple versions can be found here: https://github.com/GaloisInc/cryptol/blob/master/.github/workflows/docs.yml, and rendered here https://galoisinc.github.io/cryptol/master/RefMan.html (see the "Doc version" selector at the bottom left).

That may be overkill for current needs, but this allows for user selection of a version (with a supporting selector) including active PR's in case there are multiple release versions.

@RyanGlScott RyanGlScott added the CI Continuous integration label Nov 15, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CI Continuous integration
Projects
None yet
Development

No branches or pull requests

3 participants