Bugzilla to GitHub Issues Migration

[Mike Parker]

On Friday, 23 June 2023 at 12:31:39 UTC, Timon Gehr wrote:
> On 6/23/23 11:53, Robert Schadek wrote:
>>>

>
> Yes, unfortunately it is true that many people won't report 
> issues on bugzilla. Preserving the existing issues is still 
> really important as well. Those are issues reported by 
> _enthusiastic people who let themselves be assed to report on 
> bugzilla_, and we owe them to treat their issues well. In 
> particular, I think moving issues to github issues and giving 
> all the github contributions/authorship for those issues to 
> yourself and Mike is a terrible way to move forward, even if 
> the issues are technically in the public domain and/or belong 
> to DLF.

For the record, I intend to create a special account for adding 
the issues to GitHub (e.g., "bugzilla_migration"). I certainly 
don't want them all in my name. I don't see how we can post them 
as the original user, though. From what I understand, it requires 
the id and a token.