On Mon, Nov 21, 2022 at 11:41 PM Tom Lane <tgl@sss.pgh.pa.us> wrote:
Andrew Dunstan <andrew@dunslane.net> writes: > On 2022-11-21 Mo 15:58, Tom Lane wrote: >> But if we're trying to improve matters in this area, this doesn't seem >> like quite the way to go.
> Well, 5 minutes was originally chosen because it was sufficient for the > purpose for which up to now the server used its mirror. Now we have > added a new purpose we can certainly revisit that. Shall I try 2 minutes > or go down to 1?
Actually, if we implement a webhook to update this, the server could stop doing speculative git pulls too, no?
That would be the main point, yes. Saves a few hundred (or thousand) wasteful git pulls *and* reacts quicker to actual pushes. As long as you have a clear line of communications between the machines, it's basically win/win I think. That's probably why, as Thomas noticed earlier, that's what "everybody" does.
