[webkit-dev] Repository changes on git.webkit.org

[Mark Rowe]

Hi all,

If you're using our Git repository mirror hosted on git.webkit.org,  
please be aware of the following:

git://git.webkit.org/WebKit.git
will be moving to:
git://git.webkit.org/WebKit-ssh.git

This change will be happening later today.  You will want to run the  
following command in any repository which has git.webkit.org  
configured as a remote:
sed -i -e 's|git://git.webkit.org/WebKit.git|git://git.webkit.org/ 
WebKit-ssh.git|' .git/config

It is safe to run the command now as the repository exists temporarily  
at both the old and new paths.

Kind regards,

Mark