Can the build_docs.py cron be started hourly?

[JulienPalard]

The build_docs.py script has changed a lot:

• It no longer rebuilds what's not needed to rebuild.
• It dies if another builder is running.

So starting it hourly would keep fast-changing doc fresher, while using less CPU than the old "let's rebuild everything everyday" approach.

Technically starting it minutely would work too, but it would flood the logs and it would be started hundreds of times in a row just to git fetch and do nothing (if nothing changed).

Feel like hourly is a good compromise.