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 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. I contacted them but before I could get answer I decide to
 'split' the push. First I git reset --hard the repository back to a
 commit from 2008, pushed this, then reset --hard to 2009 and pushed
 this, and so on.

 In the middle of the process the folks from github increased our push
 limit to 20GB and David (barrbrain) was kind enough to push one last
 sync, getting us back to 2012. After that I kept the syncing manullay
 for a few hours but now the repository is being updated automatically
 every 5 minutes to stay in sync with git.webkit.org .

 I will now coordinate with William so we can get Apple pushing to the
 mirror at the same time they push to git.webkit.org .

 Thanks everyone that got involved for the help!

 Cheers,
 jesus

 2013/1/14 Jesus Sanchez-Palencia je...@webkit.org:
  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 strategy here after talking to a few people on
 #github.
  It seems that doing a git push -f to the current repository
  (https://github.com/WebKit/webkit) will actually have less impact on
  people branching/forking it on github. In other words, it should be
  less painful to rebase your fork on github for the new hashes after
  I'm done with the setup.
 
  I will let you know when the switching is done.
 
  Cheers,
  jesus
 
 
  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.
 
  People that are using the current github repository will probably have
  to re-clone and rebase their branches.
 
  This won't affect git.webkit.org or any other official WebKit
 repository.
 
 
  Cheers,
  jesus
 
 
 
  2012/12/11 Jesus Sanchez-Palencia jesus.palen...@openbossa.org:
  Hi,
 
  2012/12/4 Tor Arne Vestbø tor.arne.ves...@digia.com:
 
  Bill, what do you think about pushing the official SVN import to
 GitHub as
  well?
 
  tor arne
 
  Any updates about this?
 
  Cheers,
  jesus
 
 
 
 
  So we might be able to rename the existing one and ask github to
 pull
  our git.webkit.org http://git.webkit.org repository into
 
  github/WebKit/webkit.
  Apparently Apache takes that way: https://github.com/apache
  The mirroring icon indicates kind of official-ness.
 
  I don't know how long their mirroring delay is, though.
 
 
 
  On Sat, Dec 1, 2012 at 12:07 AM, Tor Arne Vestbø
  tor.arne.ves...@digia.com mailto:tor.arne.ves...@digia.com
 wrote:
 
  On 11/28/12 16:55 , Adam Barth wrote:
 
  My sense is that the WebKit community would prefer that the
  hashes in
  GitHub match the hashes in git.webkit.org
  http://git.webkit.org so that folks can more
 
  easily move branches between the two.  For my part, I've
  switched over
  to using GitHub exclusive of git.webkit.org
  http://git.webkit.org, so the the difference in
 
  hashes aren't an issue for me, but I can understand why
 they'd be
  problematic for other people.
 
 
  Yepp, agreed. Let's switch it over.
 
 
  After the force-push, would you still be able to push
 updates
  automatically?  If so, you can switch the hashes whenever is
  convenient for you.  (It might be nice to announce the
 date/time
  on
  this list so that folks aren't taken by surprise.)
 
 
  The mirror is also pushed to
 http://gitorious.org/webkit/__webkit
  http://gitorious.org/webkit/webkit, which I was planning to
 keep
 
  as is for now, so that would mean setting up an extra mirroring
 for
  the non-author-rewritten history :/ Also, the server I run this
 on
  has a somewhat uncertain future. With that in mind it's probably
  easier to just push directly from the same import that's pushed
 to
  git.webkit.org http://git.webkit.org, and make the GitHub
 mirror
 
  an official mirror?
 
  tor arne
 
  _
  webkit-dev mailing list
  webkit-dev@lists.webkit.org mailto:webkit-dev@lists.webkit.org
 
  http://lists.webkit.org/__mailman/listinfo/webkit-dev
  http://lists.webkit.org/mailman/listinfo/webkit-dev
 
 
 
 
 
  

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 to push a 
small amount - at least that's how it worked for me.


Dominik
___
webkit-dev mailing list
webkit-dev@lists.webkit.org
http://lists.webkit.org/mailman/listinfo/webkit-dev


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
on top of that, but that's a start.

On Thu, Jan 17, 2013 at 4:00 AM, Dominik Röttsches
dominik.rottsc...@intel.com wrote:
 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 to push a small
 amount - at least that's how it worked for me.

 Dominik

 ___
 webkit-dev mailing list
 webkit-dev@lists.webkit.org
 http://lists.webkit.org/mailman/listinfo/webkit-dev

___
webkit-dev mailing list
webkit-dev@lists.webkit.org
http://lists.webkit.org/mailman/listinfo/webkit-dev


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 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
on top of that, but that's a start.

On Thu, Jan 17, 2013 at 4:00 AM, Dominik Röttsches
dominik.rottsc...@intel.com wrote:

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 to push a  
small

amount - at least that's how it worked for me.

Dominik

___
webkit-dev mailing list
webkit-dev@lists.webkit.org
http://lists.webkit.org/mailman/listinfo/webkit-dev


___
webkit-dev mailing list
webkit-dev@lists.webkit.org
http://lists.webkit.org/mailman/listinfo/webkit-dev



--
pablo flouret
motorola | webkit / browser team
___
webkit-dev mailing list
webkit-dev@lists.webkit.org
http://lists.webkit.org/mailman/listinfo/webkit-dev


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. I contacted them but before I could get answer I decide to
'split' the push. First I git reset --hard the repository back to a
commit from 2008, pushed this, then reset --hard to 2009 and pushed
this, and so on.

In the middle of the process the folks from github increased our push
limit to 20GB and David (barrbrain) was kind enough to push one last
sync, getting us back to 2012. After that I kept the syncing manullay
for a few hours but now the repository is being updated automatically
every 5 minutes to stay in sync with git.webkit.org .

I will now coordinate with William so we can get Apple pushing to the
mirror at the same time they push to git.webkit.org .

Thanks everyone that got involved for the help!

Cheers,
jesus

2013/1/14 Jesus Sanchez-Palencia je...@webkit.org:
 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 strategy here after talking to a few people on #github.
 It seems that doing a git push -f to the current repository
 (https://github.com/WebKit/webkit) will actually have less impact on
 people branching/forking it on github. In other words, it should be
 less painful to rebase your fork on github for the new hashes after
 I'm done with the setup.

 I will let you know when the switching is done.

 Cheers,
 jesus


 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.

 People that are using the current github repository will probably have
 to re-clone and rebase their branches.

 This won't affect git.webkit.org or any other official WebKit repository.


 Cheers,
 jesus



 2012/12/11 Jesus Sanchez-Palencia jesus.palen...@openbossa.org:
 Hi,

 2012/12/4 Tor Arne Vestbø tor.arne.ves...@digia.com:

 Bill, what do you think about pushing the official SVN import to GitHub as
 well?

 tor arne

 Any updates about this?

 Cheers,
 jesus




 So we might be able to rename the existing one and ask github to pull
 our git.webkit.org http://git.webkit.org repository into

 github/WebKit/webkit.
 Apparently Apache takes that way: https://github.com/apache
 The mirroring icon indicates kind of official-ness.

 I don't know how long their mirroring delay is, though.



 On Sat, Dec 1, 2012 at 12:07 AM, Tor Arne Vestbø
 tor.arne.ves...@digia.com mailto:tor.arne.ves...@digia.com wrote:

 On 11/28/12 16:55 , Adam Barth wrote:

 My sense is that the WebKit community would prefer that the
 hashes in
 GitHub match the hashes in git.webkit.org
 http://git.webkit.org so that folks can more

 easily move branches between the two.  For my part, I've
 switched over
 to using GitHub exclusive of git.webkit.org
 http://git.webkit.org, so the the difference in

 hashes aren't an issue for me, but I can understand why they'd be
 problematic for other people.


 Yepp, agreed. Let's switch it over.


 After the force-push, would you still be able to push updates
 automatically?  If so, you can switch the hashes whenever is
 convenient for you.  (It might be nice to announce the date/time
 on
 this list so that folks aren't taken by surprise.)


 The mirror is also pushed to http://gitorious.org/webkit/__webkit
 http://gitorious.org/webkit/webkit, which I was planning to keep

 as is for now, so that would mean setting up an extra mirroring for
 the non-author-rewritten history :/ Also, the server I run this on
 has a somewhat uncertain future. With that in mind it's probably
 easier to just push directly from the same import that's pushed to
 git.webkit.org http://git.webkit.org, and make the GitHub mirror

 an official mirror?

 tor arne

 _
 webkit-dev mailing list
 webkit-dev@lists.webkit.org mailto:webkit-dev@lists.webkit.org
 http://lists.webkit.org/__mailman/listinfo/webkit-dev
 http://lists.webkit.org/mailman/listinfo/webkit-dev





 ___
 webkit-dev mailing list
 webkit-dev@lists.webkit.org
 http://lists.webkit.org/mailman/listinfo/webkit-dev


 ___
 webkit-dev mailing list
 webkit-dev@lists.webkit.org
 http://lists.webkit.org/mailman/listinfo/webkit-dev
___
webkit-dev mailing list
webkit-dev@lists.webkit.org

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

Adam


On Wed, Jan 16, 2013 at 4:55 AM, Jesus Sanchez-Palencia
je...@webkit.org wrote:
 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. I contacted them but before I could get answer I decide to
 'split' the push. First I git reset --hard the repository back to a
 commit from 2008, pushed this, then reset --hard to 2009 and pushed
 this, and so on.

 In the middle of the process the folks from github increased our push
 limit to 20GB and David (barrbrain) was kind enough to push one last
 sync, getting us back to 2012. After that I kept the syncing manullay
 for a few hours but now the repository is being updated automatically
 every 5 minutes to stay in sync with git.webkit.org .

 I will now coordinate with William so we can get Apple pushing to the
 mirror at the same time they push to git.webkit.org .

 Thanks everyone that got involved for the help!

 Cheers,
 jesus

 2013/1/14 Jesus Sanchez-Palencia je...@webkit.org:
 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 strategy here after talking to a few people on #github.
 It seems that doing a git push -f to the current repository
 (https://github.com/WebKit/webkit) will actually have less impact on
 people branching/forking it on github. In other words, it should be
 less painful to rebase your fork on github for the new hashes after
 I'm done with the setup.

 I will let you know when the switching is done.

 Cheers,
 jesus


 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.

 People that are using the current github repository will probably have
 to re-clone and rebase their branches.

 This won't affect git.webkit.org or any other official WebKit repository.


 Cheers,
 jesus



 2012/12/11 Jesus Sanchez-Palencia jesus.palen...@openbossa.org:
 Hi,

 2012/12/4 Tor Arne Vestbø tor.arne.ves...@digia.com:

 Bill, what do you think about pushing the official SVN import to GitHub 
 as
 well?

 tor arne

 Any updates about this?

 Cheers,
 jesus




 So we might be able to rename the existing one and ask github to pull
 our git.webkit.org http://git.webkit.org repository into

 github/WebKit/webkit.
 Apparently Apache takes that way: https://github.com/apache
 The mirroring icon indicates kind of official-ness.

 I don't know how long their mirroring delay is, though.



 On Sat, Dec 1, 2012 at 12:07 AM, Tor Arne Vestbø
 tor.arne.ves...@digia.com mailto:tor.arne.ves...@digia.com wrote:

 On 11/28/12 16:55 , Adam Barth wrote:

 My sense is that the WebKit community would prefer that the
 hashes in
 GitHub match the hashes in git.webkit.org
 http://git.webkit.org so that folks can more

 easily move branches between the two.  For my part, I've
 switched over
 to using GitHub exclusive of git.webkit.org
 http://git.webkit.org, so the the difference in

 hashes aren't an issue for me, but I can understand why they'd 
 be
 problematic for other people.


 Yepp, agreed. Let's switch it over.


 After the force-push, would you still be able to push updates
 automatically?  If so, you can switch the hashes whenever is
 convenient for you.  (It might be nice to announce the date/time
 on
 this list so that folks aren't taken by surprise.)


 The mirror is also pushed to http://gitorious.org/webkit/__webkit
 http://gitorious.org/webkit/webkit, which I was planning to keep

 as is for now, so that would mean setting up an extra mirroring for
 the non-author-rewritten history :/ Also, the server I run this on
 has a somewhat uncertain future. With that in mind it's probably
 easier to just push directly from the same import that's pushed to
 git.webkit.org http://git.webkit.org, and make the GitHub mirror

 an official mirror?

 tor arne

 _
 webkit-dev mailing list
 webkit-dev@lists.webkit.org mailto:webkit-dev@lists.webkit.org
 http://lists.webkit.org/__mailman/listinfo/webkit-dev
 http://lists.webkit.org/mailman/listinfo/webkit-dev





 

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

 Adam


 On Wed, Jan 16, 2013 at 4:55 AM, Jesus Sanchez-Palencia
 je...@webkit.org wrote:
 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. I contacted them but before I could get answer I decide to
 'split' the push. First I git reset --hard the repository back to a
 commit from 2008, pushed this, then reset --hard to 2009 and pushed
 this, and so on.

 In the middle of the process the folks from github increased our push
 limit to 20GB and David (barrbrain) was kind enough to push one last
 sync, getting us back to 2012. After that I kept the syncing manullay
 for a few hours but now the repository is being updated automatically
 every 5 minutes to stay in sync with git.webkit.org .

 I will now coordinate with William so we can get Apple pushing to the
 mirror at the same time they push to git.webkit.org .

 Thanks everyone that got involved for the help!

 Cheers,
 jesus

 2013/1/14 Jesus Sanchez-Palencia je...@webkit.org:
 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 strategy here after talking to a few people on #github.
 It seems that doing a git push -f to the current repository
 (https://github.com/WebKit/webkit) will actually have less impact on
 people branching/forking it on github. In other words, it should be
 less painful to rebase your fork on github for the new hashes after
 I'm done with the setup.

 I will let you know when the switching is done.

 Cheers,
 jesus


 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.

 People that are using the current github repository will probably have
 to re-clone and rebase their branches.

 This won't affect git.webkit.org or any other official WebKit repository.


 Cheers,
 jesus



 2012/12/11 Jesus Sanchez-Palencia jesus.palen...@openbossa.org:
 Hi,

 2012/12/4 Tor Arne Vestbø tor.arne.ves...@digia.com:

 Bill, what do you think about pushing the official SVN import to GitHub 
 as
 well?

 tor arne

 Any updates about this?

 Cheers,
 jesus




 So we might be able to rename the existing one and ask github to pull
 our git.webkit.org http://git.webkit.org repository into

 github/WebKit/webkit.
 Apparently Apache takes that way: https://github.com/apache
 The mirroring icon indicates kind of official-ness.

 I don't know how long their mirroring delay is, though.



 On Sat, Dec 1, 2012 at 12:07 AM, Tor Arne Vestbø
 tor.arne.ves...@digia.com mailto:tor.arne.ves...@digia.com wrote:

 On 11/28/12 16:55 , Adam Barth wrote:

 My sense is that the WebKit community would prefer that the
 hashes in
 GitHub match the hashes in git.webkit.org
 http://git.webkit.org so that folks can more

 easily move branches between the two.  For my part, I've
 switched over
 to using GitHub exclusive of git.webkit.org
 http://git.webkit.org, so the the difference in

 hashes aren't an issue for me, but I can understand why they'd 
 be
 problematic for other people.


 Yepp, agreed. Let's switch it over.


 After the force-push, would you still be able to push updates
 automatically?  If so, you can switch the hashes whenever is
 convenient for you.  (It might be nice to announce the 
 date/time
 on
 this list so that folks aren't taken by surprise.)


 The mirror is also pushed to http://gitorious.org/webkit/__webkit
 http://gitorious.org/webkit/webkit, which I was planning to keep

 as is for now, so that would mean setting up an extra mirroring for
 the non-author-rewritten history :/ Also, the server I run this on
 has a somewhat uncertain future. With that in mind it's probably
 easier to just push directly from the same import that's pushed to
 git.webkit.org http://git.webkit.org, and make the GitHub mirror

 an official mirror?

 tor arne

 _
 webkit-dev mailing list
   

[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
discussed in the past.

Since last week me, Tor Arne, William Siegrist, Adam Barth and Lucas
Forschler have been discussing the steps to move on with this and
since no one has raised any issues so far on previous discussions, I
will start this today.

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.

People that are using the current github repository will probably have
to re-clone and rebase their branches.

This won't affect git.webkit.org or any other official WebKit repository.


Cheers,
jesus



2012/12/11 Jesus Sanchez-Palencia jesus.palen...@openbossa.org:
 Hi,

 2012/12/4 Tor Arne Vestbø tor.arne.ves...@digia.com:

 Bill, what do you think about pushing the official SVN import to GitHub as
 well?

 tor arne

 Any updates about this?

 Cheers,
 jesus




 So we might be able to rename the existing one and ask github to pull
 our git.webkit.org http://git.webkit.org repository into

 github/WebKit/webkit.
 Apparently Apache takes that way: https://github.com/apache
 The mirroring icon indicates kind of official-ness.

 I don't know how long their mirroring delay is, though.



 On Sat, Dec 1, 2012 at 12:07 AM, Tor Arne Vestbø
 tor.arne.ves...@digia.com mailto:tor.arne.ves...@digia.com wrote:

 On 11/28/12 16:55 , Adam Barth wrote:

 My sense is that the WebKit community would prefer that the
 hashes in
 GitHub match the hashes in git.webkit.org
 http://git.webkit.org so that folks can more

 easily move branches between the two.  For my part, I've
 switched over
 to using GitHub exclusive of git.webkit.org
 http://git.webkit.org, so the the difference in

 hashes aren't an issue for me, but I can understand why they'd be
 problematic for other people.


 Yepp, agreed. Let's switch it over.


 After the force-push, would you still be able to push updates
 automatically?  If so, you can switch the hashes whenever is
 convenient for you.  (It might be nice to announce the date/time
 on
 this list so that folks aren't taken by surprise.)


 The mirror is also pushed to http://gitorious.org/webkit/__webkit
 http://gitorious.org/webkit/webkit, which I was planning to keep

 as is for now, so that would mean setting up an extra mirroring for
 the non-author-rewritten history :/ Also, the server I run this on
 has a somewhat uncertain future. With that in mind it's probably
 easier to just push directly from the same import that's pushed to
 git.webkit.org http://git.webkit.org, and make the GitHub mirror

 an official mirror?

 tor arne

 _
 webkit-dev mailing list
 webkit-dev@lists.webkit.org mailto:webkit-dev@lists.webkit.org
 http://lists.webkit.org/__mailman/listinfo/webkit-dev
 http://lists.webkit.org/mailman/listinfo/webkit-dev





 ___
 webkit-dev mailing list
 webkit-dev@lists.webkit.org
 http://lists.webkit.org/mailman/listinfo/webkit-dev


 ___
 webkit-dev mailing list
 webkit-dev@lists.webkit.org
 http://lists.webkit.org/mailman/listinfo/webkit-dev
___
webkit-dev mailing list
webkit-dev@lists.webkit.org
http://lists.webkit.org/mailman/listinfo/webkit-dev


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 Apple can set
this up from the same machine that git pushes to git.webkit.org.


Great to see this, thanks!

Dominik

___
webkit-dev mailing list
webkit-dev@lists.webkit.org
http://lists.webkit.org/mailman/listinfo/webkit-dev


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 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
 discussed in the past.

 Since last week me, Tor Arne, William Siegrist, Adam Barth and Lucas
 Forschler have been discussing the steps to move on with this and
 since no one has raised any issues so far on previous discussions, I
 will start this today.

 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.

 People that are using the current github repository will probably have
 to re-clone and rebase their branches.

 This won't affect git.webkit.org or any other official WebKit repository.


 Cheers,
 jesus



 2012/12/11 Jesus Sanchez-Palencia jesus.palen...@openbossa.org:
 Hi,

 2012/12/4 Tor Arne Vestbø tor.arne.ves...@digia.com:

 Bill, what do you think about pushing the official SVN import to GitHub as
 well?

 tor arne

 Any updates about this?

 Cheers,
 jesus




 So we might be able to rename the existing one and ask github to pull
 our git.webkit.org http://git.webkit.org repository into

 github/WebKit/webkit.
 Apparently Apache takes that way: https://github.com/apache
 The mirroring icon indicates kind of official-ness.

 I don't know how long their mirroring delay is, though.



 On Sat, Dec 1, 2012 at 12:07 AM, Tor Arne Vestbø
 tor.arne.ves...@digia.com mailto:tor.arne.ves...@digia.com wrote:

 On 11/28/12 16:55 , Adam Barth wrote:

 My sense is that the WebKit community would prefer that the
 hashes in
 GitHub match the hashes in git.webkit.org
 http://git.webkit.org so that folks can more

 easily move branches between the two.  For my part, I've
 switched over
 to using GitHub exclusive of git.webkit.org
 http://git.webkit.org, so the the difference in

 hashes aren't an issue for me, but I can understand why they'd be
 problematic for other people.


 Yepp, agreed. Let's switch it over.


 After the force-push, would you still be able to push updates
 automatically?  If so, you can switch the hashes whenever is
 convenient for you.  (It might be nice to announce the date/time
 on
 this list so that folks aren't taken by surprise.)


 The mirror is also pushed to http://gitorious.org/webkit/__webkit
 http://gitorious.org/webkit/webkit, which I was planning to keep

 as is for now, so that would mean setting up an extra mirroring for
 the non-author-rewritten history :/ Also, the server I run this on
 has a somewhat uncertain future. With that in mind it's probably
 easier to just push directly from the same import that's pushed to
 git.webkit.org http://git.webkit.org, and make the GitHub mirror

 an official mirror?

 tor arne

 _
 webkit-dev mailing list
 webkit-dev@lists.webkit.org mailto:webkit-dev@lists.webkit.org
 http://lists.webkit.org/__mailman/listinfo/webkit-dev
 http://lists.webkit.org/mailman/listinfo/webkit-dev





 ___
 webkit-dev mailing list
 webkit-dev@lists.webkit.org
 http://lists.webkit.org/mailman/listinfo/webkit-dev


 ___
 webkit-dev mailing list
 webkit-dev@lists.webkit.org
 http://lists.webkit.org/mailman/listinfo/webkit-dev
___
webkit-dev mailing list
webkit-dev@lists.webkit.org
http://lists.webkit.org/mailman/listinfo/webkit-dev


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 strategy here after talking to a few people on #github.
It seems that doing a git push -f to the current repository
(https://github.com/WebKit/webkit) will actually have less impact on
people branching/forking it on github. In other words, it should be
less painful to rebase your fork on github for the new hashes after
I'm done with the setup.

I will let you know when the switching is done.

Cheers,
jesus


 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.

 People that are using the current github repository will probably have
 to re-clone and rebase their branches.

 This won't affect git.webkit.org or any other official WebKit repository.


 Cheers,
 jesus



 2012/12/11 Jesus Sanchez-Palencia jesus.palen...@openbossa.org:
 Hi,

 2012/12/4 Tor Arne Vestbø tor.arne.ves...@digia.com:

 Bill, what do you think about pushing the official SVN import to GitHub as
 well?

 tor arne

 Any updates about this?

 Cheers,
 jesus




 So we might be able to rename the existing one and ask github to pull
 our git.webkit.org http://git.webkit.org repository into

 github/WebKit/webkit.
 Apparently Apache takes that way: https://github.com/apache
 The mirroring icon indicates kind of official-ness.

 I don't know how long their mirroring delay is, though.



 On Sat, Dec 1, 2012 at 12:07 AM, Tor Arne Vestbø
 tor.arne.ves...@digia.com mailto:tor.arne.ves...@digia.com wrote:

 On 11/28/12 16:55 , Adam Barth wrote:

 My sense is that the WebKit community would prefer that the
 hashes in
 GitHub match the hashes in git.webkit.org
 http://git.webkit.org so that folks can more

 easily move branches between the two.  For my part, I've
 switched over
 to using GitHub exclusive of git.webkit.org
 http://git.webkit.org, so the the difference in

 hashes aren't an issue for me, but I can understand why they'd be
 problematic for other people.


 Yepp, agreed. Let's switch it over.


 After the force-push, would you still be able to push updates
 automatically?  If so, you can switch the hashes whenever is
 convenient for you.  (It might be nice to announce the date/time
 on
 this list so that folks aren't taken by surprise.)


 The mirror is also pushed to http://gitorious.org/webkit/__webkit
 http://gitorious.org/webkit/webkit, which I was planning to keep

 as is for now, so that would mean setting up an extra mirroring for
 the non-author-rewritten history :/ Also, the server I run this on
 has a somewhat uncertain future. With that in mind it's probably
 easier to just push directly from the same import that's pushed to
 git.webkit.org http://git.webkit.org, and make the GitHub mirror

 an official mirror?

 tor arne

 _
 webkit-dev mailing list
 webkit-dev@lists.webkit.org mailto:webkit-dev@lists.webkit.org
 http://lists.webkit.org/__mailman/listinfo/webkit-dev
 http://lists.webkit.org/mailman/listinfo/webkit-dev





 ___
 webkit-dev mailing list
 webkit-dev@lists.webkit.org
 http://lists.webkit.org/mailman/listinfo/webkit-dev


 ___
 webkit-dev mailing list
 webkit-dev@lists.webkit.org
 http://lists.webkit.org/mailman/listinfo/webkit-dev
___
webkit-dev mailing list
webkit-dev@lists.webkit.org
http://lists.webkit.org/mailman/listinfo/webkit-dev