Doc gitlab ci

This will allow to keep different versions of the documentation based on git tags.

Look at the example: example

The code is based on shell scripts, and does something tricky, maybe fragile, but it works and gitlab does not provide anything for this problem (there is an issue open since years).