Doc details

The doc is built thanks to the Makefile's goal docker-deploy-doc.

This goal builds the the content of docs/ and commit the result in the gh-deploy branch.

To be able to push the doc on Github, you will need to have the SSH configuration and keys in your $HOME/.ssh.

The doc is available on the domain describes in docs/CNAME file.

Of course the CNAME should be configured as explained in the official Github doc.

The doc is deployed for each merge on master.