Documentation build clutters git pull

[wysiwyng]

Currently the Doxygen documentation is built and updated on every push to this repo, and the resulting html files committed to the gh-pages branch in this repo. While this practice guarantees up-to-date documentation, it also implies that this gh-pages branch is always updated on your local working folder if you run a git pull, resulting in a download of several 100 Mbytes.

Some ideas are:

• Trigger documentation build manually, or only if tags are pushed
• Host the documentation elsewhere (VP-Vibes? Wiki Repository?)

[wysiwyng]

In addition to documentation, the performance regression testing introduced with #77 also needs a place to store its data. Currently, this is the benchmark_results branch on the main repository. As above, doing things this way is easy but clutters the repository with unrelated stuff.

For the performance history in particular, storing it in the wiki repository of this repo should work nicely. Manual accessibility would suffer of course, unless this data is stored visibly embedded in some actual wiki page, instead of plain JSON.