Skip to content

Publish documentation on github.io #140

Description

@ezio-melotti

By reading https://www.docslikecode.com/articles/github-pages-python-sphinx/ and https://docs.github.com/en/pages/getting-started-with-github-pages/changing-the-visibility-of-your-github-pages-site it seems it should be possible to build the docs and publish them on a private github.io page. We could set up a GitHub action that is auto-triggered when something is pushed to docs/, that builds the docs and publishes them.

There is also a docker container that can be pulled to build the docs, and perhaps some GitHub action that does that out of the box already. I've also considered building the PDF, but it needs over 1GB of latex dependencies to be built, so it might not be worth it to automate it.

Metadata

Metadata

Assignees

No one assigned

    Labels

    featureA new featureinfrastructureDocker, GCP, GitHub actions, etc.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions