On Wed, 18 Aug 2021 at 12:45, Alex Miller <alex@puredanger.com> 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