(files from previous build were kept on the server, with outdated/garbled
information)
The documentation update script now wipes build/doc/html
before rebuilding stuff. Most of the time/cpu consuming is spent in
compiling snippets, so we don't loose that much.
Thomas Capricelli
aba50d842e