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

2013-01-25 Thread Jesus Sanchez-Palencia
Sorry, we have been facing network issues here for the past few days... Anyway, should be fixed now and it is pushing the current git.webkit.org HEAD already. Cheers, jesus 2013/1/25 Florin Malita : > Looks like mirroring stopped on 1/23 (last commit: > https://github.com/WebKit/webkit/commit/d5c

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

2013-01-25 Thread Florin Malita
Looks like mirroring stopped on 1/23 (last commit: https://github.com/WebKit/webkit/commit/d5c4f2bd4a80b397eade1ee53b39d738e5656598 ). Jesus, can you take a look? Thanks, Florin On Wed, Jan 16, 2013 at 7:55 AM, Jesus Sanchez-Palencia wrote: > Hi, > > The mirror is finally ready again: https://

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

2013-01-17 Thread Pablo Flouret
Maybe "git rebase --onto" would help, if only a bit? http://git-scm.com/book/en/Git-Branching-Rebasing#More-Interesting-Rebases /pf On Thu, 17 Jan 2013 13:13:44 -0800, Eric Seidel wrote: Yes, but I'm more interested in rebasing my existing github branches. :) But you're right, I could proba

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

2013-01-17 Thread Eric Seidel
Yes, but I'm more interested in rebasing my existing github branches. :) But you're right, I could probably run Tools/Scripts/sync-master-with-upstream from my existing git.webkit.org checkout and not have to download anything. I'd still have a bunch of github branches which I can't easily rebase

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

2013-01-17 Thread Dominik Röttsches
On 01/16/2013 10:07 PM, Eric Seidel wrote: Do we know if there is a way to re-write our existing forks w/o pulling the whole repo down, just to push it back up again? If you make the new github mirror fork a remote for your existing git.webkit.org clone and push from there you would only need

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

2013-01-16 Thread Eric Seidel
Do we know if there is a way to re-write our existing forks w/o pulling the whole repo down, just to push it back up again? :) On Wed, Jan 16, 2013 at 11:51 AM, Adam Barth wrote: > If you were using GitHub to contribute to WebKit previously, you might > want to delete your fork of https://github.

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

2013-01-16 Thread Adam Barth
If you were using GitHub to contribute to WebKit previously, you might want to delete your fork of https://github.com/WebKit/webkit and re-fork https://github.com/WebKit/webkit. It's also possible to push a force update to your repository that re-writes the hashes, but I found that re-forking was

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

2013-01-16 Thread Jesus Sanchez-Palencia
Hi, The mirror is finally ready again: https://github.com/WebKit/webkit It now follows the same hashes of git.webkit.org. People who have forked this repository on github before will now have to rebase their branches. I was hold back a bit because Github wasn't allowing me to push more than 2GB.

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

2013-01-14 Thread Jesus Sanchez-Palencia
Hi, Just yet another quick heads-up: > 2013/1/14 Jesus Sanchez-Palencia : >> 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 had to change my strategy h

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

2013-01-14 Thread Jesus Sanchez-Palencia
The github repository has stopped being updated and will remain like that for the next hours until I have finished the new setup. cheers, jesus 2013/1/14 Jesus Sanchez-Palencia : > Hi, > > This email is a heads-up about the repository change we are starting > today in github. > > In summary, now

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

2013-01-14 Thread 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 Appl

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

2013-01-14 Thread Jesus Sanchez-Palencia
Hi, This email is a heads-up about the repository change we are starting today in github. In summary, now the github webkit repository will actually mirror git.webkit.org and they will finally have the same git hashes. I won't go into the benefits of this change since this has been widely discuss