Put published documentation in a separate branch

[sapetnioc]

To date, documentation published on https://populse.github.io/populse_db is located in the docs directory of master branch. This is a mess with git when one wants to modify some sources but not yet the published html. If the doc generation was tested locally (with make html), a lot of files get modified and it is difficult to tell the few ones that are modified sources from the modifications done by sphinx generator.

I propose to remove the Sphinx generated files from master branch (keeping only source files) and to keep them in a dedicated published_documentation branch that would be used by https://populse.github.io/populse_db. Modification of the documentation source would be simpler and publication of a new version of the documentation would require to start with the following commands:

git checkout published_documentation
git pull
git merge master
# create doc, commit and push as before

[servoz]

ok for me!

[denisri]

It's possible and probably better to setup an automatic docs building in the gh-pages branch, but it needs either a working travis-ci or a github action.

[sapetnioc]

Does it means that I should use gh-pages as branch name for the documentation instead of ̀published_documentation ? Is it a de-facto standard ?