On Wed, 18 Aug 2021 at 12:45, Alex Miller <[email protected]> wrote: > Eventually we'll rename the repo but it's going to break a bunch of > infrastructure so I'm not super eager about that. :)
AFAIK, GitHub automatically provides redirects for renamed repos. In my own experience, they work quite well... --Leandro
