Issues (possibly) caused by the current duration of the site generation script

[JJ]

The problem

There are sometimes subtle problems of the type search.js is not still updated with the latest changes to the documentation; this does not take long, however, and is rarely noticed except by the person that has done the change.

But the main problem is that site regeneration takes now ~13 minutes, while the cron job that regenerates the site is programmed to work every 5 minutes. If two push are followed closely by each other, theoretically there's a lock on some files so it shouldn't go ahead, but the fact that there are subtle errors tells me lock does not work all across the files, or there's something else we are missing.

Suggestions

Obvious suggestion would be to change the cronjob so that it is more in sync with the time it takes to regenerate the site, but that's going to work as long as the generation time does not increase. Also revise the process of generation and synchronisation to avoid these problems. And, of course, try to make the generation process faster by using caches or other devices.
This would be related to #1823 mainly.

[coke]

It's not theoretical; there's a lock:

*/5     *       *       *       * PATH=/usr/local/bin:/usr/bin:/bin
                flock -n ~/update.lock -c ./doc/util/update-and-sync > update.log 2>&1

[JJ]

Closing this since it's no longer generated this way.