On Mon, Nov 21, 2022 at 11:41 PM Tom Lane <t...@sss.pgh.pa.us> wrote:
> Andrew Dunstan <and...@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. -- Magnus Hagander Me: https://www.hagander.net/ <http://www.hagander.net/> Work: https://www.redpill-linpro.com/ <http://www.redpill-linpro.com/>
