> This also remind me that we'll have to do something about this git-mirror. We > can either: > (1) - make it empty with a link to the new git repo > (2) - keep it as is (i.e., no sync) for a short period and then proceed as (1) > (3) - delete it and recreate it as a synced mirror of the new repo, and then > after a short period proceed as (1)
> If I'm not mistaken option (3) will probably break all users of this mirror, > so that's probably not the best option! I am one of the users of the current github mirror, and yes, as I understand it option 3 isn’t really an option because of the re-written history. I see no point in it. I think option (1) is best. I look forward to swapping over to the gitlab mirror. Toby
