#221 Fix doc publication.
Merged by ralph. Opened by ralph.
git-branch  into  master

Download 221.patch

We can use GIT_BRANCH now that @jmolet updated our jenkins plugins.

Pull-Request has been merged by ralph

Metadata