Re: [webkit-dev] Github vs. git.webkit.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] Github vs. git.webkit.org
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
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
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/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
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
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
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
[webkit-dev] Github vs. git.webkit.org
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
Re: [webkit-dev] Github vs. git.webkit.org
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
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
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
