WEB/DOC link to dev docs instead of contributing docs in the menu #12885
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Pet peeve of mine:
Right now the "Documentation" page links to the developer docs, while the menu links to "developers/contributing". All of the other menu entries correspond to one of the "big tocs" shown on the "Documentation" page: API, User Guide, Tutorial etc. But "Contributing" links into "developers/contributing" making the "developers" docs harder to find, which also means they are in worse shape then the overall docs.
I think we should link to the higher level toc in the menu to be consistent with the "Documentation" page. We might want to reorder the items in the "Developer" toc, though (like putting installation above contributing maybe?). I didn't do that here.