Building documentation

edit

Building documentation

edit

The build_docs executable can be used to build the documentation from a locally checked out repository, or to build all the documentation that will be uploaded to the website.