Bugzilla to GitHub Issues Migration

[Mike Parker]

On Friday, 23 June 2023 at 15:52:16 UTC, Timon Gehr wrote:

> My preference order:
> 1. Migrate all information that has a correspondence on github 
> perfectly

>
> Of course, that's just my preference, not all of those are the 
> same amount of effort, and some effort has already been spent. 
> It would be great to explore Vladimir's suggestions. If we can 
> do what LLVM did, that would be awesome.

So we've put the brakes on things for now. Robert is going to 
reach out to GitHub to see if they can do something for us like 
they did for LLVM. Then we'll hopefully be able to push the 
issues to GitHub under the original poster's handle. Of the 
issues raised here, that's the one thing we can't manage on our 
own.