Re: gitlab out of sync with sourceforge and github repositories

["Daniel Shahaf" <d.s@daniel.shahaf.name>]

Bart Schaefer wrote on Sat, 17 Dec 2022 19:57 +00:00:
> On Fri, Dec 16, 2022 at 1:05 PM Jim <linux.tech.guy@gmail.com> wrote:
>>
>> github
>> zsh-5.9-91-g1de8baded
>>
>> gitlab
>> zsh-5.9-85-g67d4bf5bb
>>
>> sourceforge
>> zsh-5.9-91-g1de8baded
>
> I think this is because Oliver and/or Daniel is/are manually updating
> gitlab, so its always going to be one attention-span behind.
>

Not me.  Oliver?

> On Thu, Dec 15, 2022 at 1:26 PM Daniel Shahaf <d.s@daniel.shahaf.name> wrote:
>>
>> Actually, I do wonder why we don't use GitLab's built-in mirroring
>> thing.  Perhaps in order to allow people to submit completion patches to
>> either GitHub or GitLab at their choice?
>
> How would where the patches are submitted affect this?  We're always
> going to apply them back on the sourceforge origin.  Conflicting
> patches for the same completion?

I'm not worried about conflicting patches; that possibility comes
with the territory.

Rather, I was wondering whether "make <this> GL repository a mirror of
<this> GH repository" might delete GL heads corresponding to merge
requests (MRs), since they don't exist on the GH end being pulled from.
(Cf. rsync's --delete option)

Now, I'm not even sure whether the lag observed this week was a one-time
thing or not.  However, should we determine that the GitLab mirror's
settings need to be changed, Oliver and I can effect such changes.

Cheers,

Daniel