Development notes

This documentation is build with the script from this gh-pages branch. That script builds the documentation from each relevant branches and commits it to the gh-pages branch for publication.

To be able to run, you need the following:

Then run ./ from the root of this repository in the gh-pages branch. That should update the documentation, which you can then push.