The workflow to edit the page would either way not be a simple click to
an edit page. But you'd have to fork the repo, sign a CLA, and then do a
PR against the correct version. So I decided to remove it.
This commit introduces GitHub Actions to build the docs and deploy them
to GitHub Pages with the following behavior:
* The job will only be triggered for pushes to the branches 'develop' or
those starting with 'v' and changes to the 'docs'-folder in order to
avoid excessive triggering.
* Jobs that are triggered concurrently on different branches are
canceled and only the last job will be executed.
The template for this action is taken from the original docusaurus
documentation (https://docusaurus.io/docs/deployment#deploying-to-github-pages).
Closes#16665
This commit contains:
* fix the build script, so that only versions are added that have a
`docusaurus.config.js`
* some refactoring so that the build script will work well with github
pages
* add configuration to the `docusaurus.config.js` to display a dropdown
menu to select a version
The behavior for the versioning is now so that 2.6 is both the 'latest'
version as well as the 'next' version. As soon as 2.7 will be built that
will be displayed as the 'next' version.
closes#16671
