Simplify documentation workflow

[jmfayard]

This is my current understanding of the problem. Please provide feedback whether I'm missing something.

I had several issues working with the documentation:

• Issue 1: in a PR reviewing a git diff of markdown usually sucks. It would be much more practical to suggest an URL where we can see the changes live.
• Issue 2: the seciont improving docs suggests to always to branch from the release branch. In fact you need to modify the docs from release or main depending on whether you are improving the doc of the current release or preparing the documentation for the next release
• Issue 3: I thought after updating the docs on release you have to merge on main. This creates lots of unnecessary git gymnastic, especially if you do multiple iterations to make a page really polished like I did with docs: magnificient page with dependencies notations)
• Issue 4: documentation works better with an a-posteriori validation than with a gate-keeper mode typical from git. There are exceptions too like site > Setup where we do want to triple check that we get it right. But we could also identify pages that would benefit to change more frequently if they were easier to edit.

[jmfayard]

Issue 1 and issue 3 can be resolved by having versioned documentation: two folders docs/main and docs/release that will be merged just before the release.

Issue 3 can be solved simply by clarifying that there is no need to merge documentation commits from release into main.

issue 1 can be probably solved by some GitHub Actions magic

Issue 2 can be improved by editing the doc, see also issue 4

Issue 4 can be solved by identifying pages that would benefit from being easier to update, and moving them to the wiki https://github.com/jmfayard/refreshVersions/wiki

Example:

• troubleshooting page
• in-progress documentation page: PR comments are a bad way to review typo and documentation suggestion, the reviewer could just edit the wiki page instead
• ...