In order to make doc fixes easier, I wonder if we could add an “Edit on GitHub” button at the top of all HTML doc pages that would link to the corresponding source file on GitHub. Apparently, there is a sphinx extension that does this:
An example of a project that uses this:
All pages on docs.readthedocs.io have an “Edit on GitHub button” at the top right-hand corner. It links to the corresponding source file, so it is useful even if you do not use the GitHub interface to edit it: you get the source file name and its complete path in the openturns tree.