Re: [webkit-dev] Github vs. git.webkit.org

2012-12-11 Thread Jesus Sanchez-Palencia
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] Github vs. git.webkit.org

2012-12-04 Thread Tor Arne Vestbø

On 11/30/12 23:59 , Hajime Morrita wrote:

It looks github supports mirroring by pulling a repo from official location.
http://stackoverflow.com/questions/11370239/creating-an-official-github-mirror


Ah, didn't know they provided that service, nice. I'm a bit worried 
about the sync delay though, as you say.


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


tor arne



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


Re: [webkit-dev] Github vs. git.webkit.org

2012-11-30 Thread Tor Arne Vestbø

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 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, 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, 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, and make the GitHub mirror an official mirror?


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


Re: [webkit-dev] Github vs. git.webkit.org

2012-11-30 Thread Hajime Morrita
It looks github supports mirroring by pulling a repo from official location.
http://stackoverflow.com/questions/11370239/creating-an-official-github-mirror

So we might be able to rename the existing one and ask github to pull our
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.comwrote:

 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 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, 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/**webkithttp://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, and make the GitHub mirror an official mirror?

 tor arne

 __**_
 webkit-dev mailing list
 webkit-dev@lists.webkit.org
 http://lists.webkit.org/**mailman/listinfo/webkit-devhttp://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] Github vs. git.webkit.org

2012-11-29 Thread Jesus Sanchez-Palencia
2012/11/28 Adam Barth aba...@webkit.org:
 My sense is that the WebKit community would prefer that the hashes in
 GitHub match the hashes in 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, so the the difference in
 hashes aren't an issue for me, but I can understand why they'd be
 problematic for other people.

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

 Thanks for letting us use your mirror.  I've found it very useful to
 be able to push work-in-progress branches to GitHub to share with
 folks.

+1.
If we are all set about this, it would be awesome if we could move on
with it, Tor Arne!
This would also avoid some extra work for Gergely Kis, I guess...

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


Re: [webkit-dev] Github vs. git.webkit.org

2012-11-29 Thread Gergely Kis
Hi,

Actually we already made the transition to the current github commit ids,
because github wanted to shut down our repository, if it is not a fork of
the semi-official webkit repository. Of course we will be able to
transition back to the git.webkit.org commit ids, when the transition was
made.

I am just mentioning this, that you don't have to rush anything because of
us.

Best Regards,
Gergely


On Thu, Nov 29, 2012 at 3:53 PM, Jesus Sanchez-Palencia je...@webkit.orgwrote:

 2012/11/28 Adam Barth aba...@webkit.org:
  My sense is that the WebKit community would prefer that the hashes in
  GitHub match the hashes in 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, so the the difference in
  hashes aren't an issue for me, but I can understand why they'd be
  problematic for other people.
 
  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.)
 
  Thanks for letting us use your mirror.  I've found it very useful to
  be able to push work-in-progress branches to GitHub to share with
  folks.

 +1.
 If we are all set about this, it would be awesome if we could move on
 with it, Tor Arne!
 This would also avoid some extra work for Gergely Kis, I guess...

 cheers,
 jesus
 ___
 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] Github vs. git.webkit.org

2012-11-28 Thread Tor Arne Vestbø

On 11/25/12 1:12 , Adam Barth wrote:

On Sat, Nov 24, 2012 at 1:53 PM, Gergely Kis gerg...@homejinni.com wrote:

Yes, I saw that thread, but I got confused by this other thread:
https://lists.webkit.org/pipermail/webkit-dev/2012-April/020339.html

Here most of the participants seemed to agree that moving the 2 repositories
to use the same SHA ids is the best course of action.


Unfortunately, the folks who maintain the mirror don't appear to
agree.  Given that they've been gracious enough to let us use their
mirror, it's hard for us to ask them to change how they run it.


This is not accurate.

I replied directly to you Adam based on the above mentioned thread, 
countering a few points from the thread, but closing off by saying that 
if the consensus was that syncing the mirrors was the way to go, I was 
perfectly fine with that too. I still am -- all it takes is someone 
letting me know when to stop pushing and to do the mentioned force-push.


Tor Arne

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


Re: [webkit-dev] Github vs. git.webkit.org

2012-11-28 Thread Adam Barth
On Wed, Nov 28, 2012 at 3:53 AM, Tor Arne Vestbø
tor.arne.ves...@digia.com wrote:
 On 11/25/12 1:12 , Adam Barth wrote:
 On Sat, Nov 24, 2012 at 1:53 PM, Gergely Kis gerg...@homejinni.com
 wrote:
 Yes, I saw that thread, but I got confused by this other thread:
 https://lists.webkit.org/pipermail/webkit-dev/2012-April/020339.html

 Here most of the participants seemed to agree that moving the 2
 repositories
 to use the same SHA ids is the best course of action.

 Unfortunately, the folks who maintain the mirror don't appear to
 agree.  Given that they've been gracious enough to let us use their
 mirror, it's hard for us to ask them to change how they run it.

 This is not accurate.

 I replied directly to you Adam based on the above mentioned thread,
 countering a few points from the thread, but closing off by saying that if
 the consensus was that syncing the mirrors was the way to go, I was
 perfectly fine with that too. I still am -- all it takes is someone letting
 me know when to stop pushing and to do the mentioned force-push.

Oh, I must have misunderstood your message.

My sense is that the WebKit community would prefer that the hashes in
GitHub match the hashes in 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, so the the difference in
hashes aren't an issue for me, but I can understand why they'd be
problematic for other people.

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

Thanks for letting us use your mirror.  I've found it very useful to
be able to push work-in-progress branches to GitHub to share with
folks.

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


Re: [webkit-dev] Github vs. git.webkit.org

2012-11-24 Thread Eric Seidel
This has come up in the past.  I believe the current recommended path
is to use the github.com SHAs and just live in a github-only world.

https://lists.webkit.org/pipermail/webkit-dev/2012-March/020002.html
has some discussion.
https://trac.webkit.org/wiki/UsingGitHub

I am not aware of any plan to change the SHAs in the github mirror or
git.webkit.org (which is unfortunate, but the current reality).

-eric

On Sat, Nov 24, 2012 at 3:39 PM, Gergely Kis gerg...@homejinni.com wrote:
 Hi,

 It looks like that the github mirror and git.webkit.org still has different
 SHA ids for commits. Is this final, or is the plan still to switch to the
 git.webkit.org SHA ids?

 For our MIPS staging repository we created a new mirror on github from
 git.webkit.org, and now we were asked by the github admins to reduce the
 repository to less than 1GB. I assume that if we would fork from the
 github.com/WebKit/webkit repository, then it would be fine with the github
 admins.

 However, if it is still the plan to switch to the git.webkit.org SHA ids in
 the github mirror as well, then we would like to avoid the extra work of
 rebasing our work to the github mirror commits, and then rebasing it back
 when the transition is made.

 We have to decide in the next couple days, because github will disable
 access to our repository again, so any status update on this transition plan
 would be helpful.

 Alternatively, if you have any experience with the github admins in how to
 ask for more space for webkit repositories, any advice would be very
 appreciated.

 Best Regards,
 Gergely Kis

 ___
 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] Github vs. git.webkit.org

2012-11-24 Thread Eric Seidel
Yes, I remember that thread now, and you're correct:
https://lists.webkit.org/pipermail/webkit-dev/2012-April/020494.html

One answer is to take your mirror and make it the main mirror on
GitHub instead of Tor's.

On Sat, Nov 24, 2012 at 3:53 PM, Gergely Kis gerg...@homejinni.com wrote:
 Hi,

 Yes, I saw that thread, but I got confused by this other thread:
 https://lists.webkit.org/pipermail/webkit-dev/2012-April/020339.html

 Here most of the participants seemed to agree that moving the 2 repositories
 to use the same SHA ids is the best course of action.

 In any case, if the github repo is the way to go now, then we will do the
 transition...

 Thanks,
 Gergely



 On Sat, Nov 24, 2012 at 10:48 PM, Eric Seidel e...@webkit.org wrote:

 This has come up in the past.  I believe the current recommended path
 is to use the github.com SHAs and just live in a github-only world.

 https://lists.webkit.org/pipermail/webkit-dev/2012-March/020002.html
 has some discussion.
 https://trac.webkit.org/wiki/UsingGitHub

 I am not aware of any plan to change the SHAs in the github mirror or
 git.webkit.org (which is unfortunate, but the current reality).

 -eric

 On Sat, Nov 24, 2012 at 3:39 PM, Gergely Kis gerg...@homejinni.com
 wrote:
  Hi,
 
  It looks like that the github mirror and git.webkit.org still has
  different
  SHA ids for commits. Is this final, or is the plan still to switch to
  the
  git.webkit.org SHA ids?
 
  For our MIPS staging repository we created a new mirror on github from
  git.webkit.org, and now we were asked by the github admins to reduce the
  repository to less than 1GB. I assume that if we would fork from the
  github.com/WebKit/webkit repository, then it would be fine with the
  github
  admins.
 
  However, if it is still the plan to switch to the git.webkit.org SHA ids
  in
  the github mirror as well, then we would like to avoid the extra work of
  rebasing our work to the github mirror commits, and then rebasing it
  back
  when the transition is made.
 
  We have to decide in the next couple days, because github will disable
  access to our repository again, so any status update on this transition
  plan
  would be helpful.
 
  Alternatively, if you have any experience with the github admins in how
  to
  ask for more space for webkit repositories, any advice would be very
  appreciated.
 
  Best Regards,
  Gergely Kis
 
  ___
  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] Github vs. git.webkit.org

2012-11-24 Thread Adam Barth
On Sat, Nov 24, 2012 at 1:53 PM, Gergely Kis gerg...@homejinni.com wrote:
 Yes, I saw that thread, but I got confused by this other thread:
 https://lists.webkit.org/pipermail/webkit-dev/2012-April/020339.html

 Here most of the participants seemed to agree that moving the 2 repositories
 to use the same SHA ids is the best course of action.

Unfortunately, the folks who maintain the mirror don't appear to
agree.  Given that they've been gracious enough to let us use their
mirror, it's hard for us to ask them to change how they run it.

 In any case, if the github repo is the way to go now, then we will do the
 transition...

That's likely the path of least resistance.

Adam


 On Sat, Nov 24, 2012 at 10:48 PM, Eric Seidel e...@webkit.org wrote:

 This has come up in the past.  I believe the current recommended path
 is to use the github.com SHAs and just live in a github-only world.

 https://lists.webkit.org/pipermail/webkit-dev/2012-March/020002.html
 has some discussion.
 https://trac.webkit.org/wiki/UsingGitHub

 I am not aware of any plan to change the SHAs in the github mirror or
 git.webkit.org (which is unfortunate, but the current reality).

 -eric

 On Sat, Nov 24, 2012 at 3:39 PM, Gergely Kis gerg...@homejinni.com
 wrote:
  Hi,
 
  It looks like that the github mirror and git.webkit.org still has
  different
  SHA ids for commits. Is this final, or is the plan still to switch to
  the
  git.webkit.org SHA ids?
 
  For our MIPS staging repository we created a new mirror on github from
  git.webkit.org, and now we were asked by the github admins to reduce the
  repository to less than 1GB. I assume that if we would fork from the
  github.com/WebKit/webkit repository, then it would be fine with the
  github
  admins.
 
  However, if it is still the plan to switch to the git.webkit.org SHA ids
  in
  the github mirror as well, then we would like to avoid the extra work of
  rebasing our work to the github mirror commits, and then rebasing it
  back
  when the transition is made.
 
  We have to decide in the next couple days, because github will disable
  access to our repository again, so any status update on this transition
  plan
  would be helpful.
 
  Alternatively, if you have any experience with the github admins in how
  to
  ask for more space for webkit repositories, any advice would be very
  appreciated.
 
  Best Regards,
  Gergely Kis
 
  ___
  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