Join GitHub today
GitHub is home to over 40 million developers working together to host and review code, manage projects, and build software together.Sign up
Build docs when touching docs/ and select directories in PRs #19303
We're currently generating some documentation from files outside of
I'm happy to merge this as-is since some visibility is better than no visibility, but I wanted to make sure you were aware of that, first.