[webkit-dev] Changing Github repository to mirror git.webkit.org (was Github vs. git.webkit.org)

[Dominik Röttsches]

On 01/14/2013 03:19 PM, Jesus Sanchez-Palencia wrote:
> We have decided that the best approach for this is to start a new
> repository (webkit-mirror), delete the old one
> (https://github.com/WebKit/webkit) and then rename the new repository.
>
> I will be doing the mirroring myself for while, until Apple can set
> this up from the same machine that git pushes to git.webkit.org.

Great to see this, thanks!

Dominik