`docs`

Leave the index.html and the .nojekyll files here, otherwise GitHub pages will break.

To update the docs, delete all folders inside this one and run make html in the docs_source folder.