When reading documentation on the internet one often thinks of little edits that could make the documentation better. To lower the barrier to making such edits this PR modifies the HTML documentation so that all pages have an "edit on GitHub" link. When a user clicks this link they'll be taken directly to an editor on GitHub with the source for that page. They can then make their changes, and launch a PR with those changes.
This came about because I wanted to add an additional resource to our "Recommended Development Resources" for generating ASCII file system diagrams. So in addition to modifying the configuration of the documentation, this PR also adds that link and description.
When reading documentation on the internet one often thinks of little edits that could make the documentation better. To lower the barrier to making such edits this PR modifies the HTML documentation so that all pages have an "edit on GitHub" link. When a user clicks this link they'll be taken directly to an editor on GitHub with the source for that page. They can then make their changes, and launch a PR with those changes.
This came about because I wanted to add an additional resource to our "Recommended Development Resources" for generating ASCII file system diagrams. So in addition to modifying the configuration of the documentation, this PR also adds that link and description.