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 je...@webkit.orgwrote: Hi, The mirror is finally ready

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-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

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 esei...@google.com wrote: Yes, but I'm more interested in rebasing my existing github branches. :) But you're

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-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 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 aba...@webkit.org wrote: If you were using GitHub to contribute to WebKit previously, you might want to delete your fork of

[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

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

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 je...@webkit.org: Hi, This email is a heads-up about the repository change we are starting today in github. In

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 je...@webkit.org: 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