Merge branch 'dev'

Author: bneron

.gitlab-ci.yml

@@ -57,7 +57,7 @@ pages:
     - make html
     - cd ${CI_PROJECT_DIR}
     - mv ${CI_PROJECT_DIR}/doc/build/html/ public
-    - mv htmlcov public/coverage
+    - mv coverage_html public/coverage
   artifacts:
     paths:
       - public