Skip to content

Update CI and documentation linking

André Anjos requested to merge update-ci into master

This merge request fixes a few problems with the documentation building and improves the CI:

  1. Use bob/bob.devtools (bdt) to manage environments, deployment and cleanup (removes also the old shell scripts)
  2. Update various sphinx's conf.py files on the 3 documentation projects to use better bob.extension's link_documentation()

Merge request reports