Re: Devel docs on website reloading

On Wed, Nov 18, 2020 at 1:31 PM Alvaro Herrera <alvherre@alvh.no-ip.org> wrote:
>
> On 2020-Nov-18, Magnus Hagander wrote:
>
> > It would be trivial to change this so that it only actually updates
> > pages if they have been changed.
>
> I think this means we could also check much more frequently whether a
> rebuild is needed, right?  We could do that every 30 mins or so, since
> most of the time it would be a no-op.

No that'd be unrelated. We don't have a dedicated buildfarm animal for
it, we just piggyback on the existing run, which runs on any changes,
not just docs.

-- 
 Magnus Hagander
 Me: https://www.hagander.net/
 Work: https://www.redpill-linpro.com/