Re: RFE: Migration zsh git repo to github or gitlab

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

Tomasz Kłoczko wrote on Tue, 21 Jul 2020 20:08 +00:00:
> On Tue, 21 Jul 2020 at 20:39, Mikael Magnusson <mikachu@gmail.com> wrote:
> 
> > There are already mirrors on github, for example
> > https://github.com/zsh-users/zsh
> 
> 
> Thx for the update. It would be nice to add that info to zsh web page :)

Agreed.

> What about make that repo as not only mirror but main on and enable
> submitting issue tickets?

You're coupling two independent matters: where the issue tracker lives
has nothing to do with which repository is the "main" one.  Also, you
haven't actually mentioned what purpose you think enabling github issues
would achieve.

In any case:

I don't see a reason to move the "main" repository.  Such a move
wouldn't affect anyone who doesn't have push access, other than the
mirrors' admins.

I am sceptical about enabling submitting github issues from the public.
Fewer people triage pull requests than triage emailed patches.  That
being the case, I am concerned that enabling issues would basically
leave them for Oliver and me to handle, which would be a poor way to
divide the overall maintenance workload.

The question of a bug tracker was discussed a number of times before.
The conclusion was that we'd like something that integrates with our
existing workflow.