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 rosdep documentation via GitHub Pages. #980

Open
wants to merge 4 commits into
base: master
Choose a base branch
from

Conversation

nuclearsandwich
Copy link
Contributor

@nuclearsandwich nuclearsandwich commented Aug 9, 2024

I'm considering updates to the ROS infrastructure package documentation to be maintained as part of the OSRA Infrastructure website.

I added an earthly build for docs in order to avoid adding an Actions-specific doc job.
That build supports the direct GitHub Pages upload.

To support the doc task I added an additional doc section to extras_require which I think is a pattern worth applying to the other ROS infrastructure packages as well.

In order to get docs building locally, I had to comment out the example intersphinx mapping as None is apparently no longer a valid map value.

I had to comment out the example intersphinx mapping as None is
apparently no longer a valid map value.

I also attempted to use extras_require to specify documentation
dependencies which are probably incomplete but it was enough to build on
my machine.
I prefer the now acceptable build.earth filename over for the
Filefile-style Earthfile.

Along with the build.earth I've also included a .earthlyignore file
which uses the same format as a [.dockerignore] file.
Although we are not creating distributable images ignoring spurious
files in the docker context helps cut down on cache misses invalidating
dependency layers in the build.

[.dockerignore]: https://docs.docker.com/build/concepts/context/#dockerignore-files
I thought that workflows were isolated but jobs were not. Ah well.
@nuclearsandwich nuclearsandwich changed the title Update for local documentation building. Deploy rosdep documentation via GitHub Pages. Aug 20, 2024
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.

1 participant