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

Deploy documentation online. #144

Closed
2 of 3 tasks
iago-lito opened this issue Mar 19, 2024 · 1 comment · Fixed by #146
Closed
2 of 3 tasks

Deploy documentation online. #144

iago-lito opened this issue Mar 19, 2024 · 1 comment · Fixed by #146
Labels
documentation Improvements or additions to documentation

Comments

@iago-lito
Copy link
Collaborator

iago-lito commented Mar 19, 2024

Github offers to host documentation online under the form of a website.

  • Follow gh-pages instructions to deploy documentation online as part of some CI job triggered on pushes to dev and/or main?
  • Update urls in the docs so they correctly point to help pages hosted on github. (3477e6b)
  • Enforce that the success of this deployment be required prior to merging new commits into dev. This would make the checks too heavy. Instead, and for now, just make sure that the docs do build prior to mergin dev into main.

Currently blocked on #105.

@iago-lito iago-lito added the documentation Improvements or additions to documentation label Mar 19, 2024
@iago-lito iago-lito linked a pull request Mar 19, 2024 that will close this issue
@iago-lito
Copy link
Collaborator Author

Closed by #146.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Improvements or additions to documentation
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant