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

Hi, 2012/12/4 Tor Arne Vestbø : > > 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

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,

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 Apac

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 t

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

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

2012/11/28 Adam Barth : > 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 diffe

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

On Wed, Nov 28, 2012 at 3:53 AM, Tor Arne Vestbø wrote: > On 11/25/12 1:12 , Adam Barth wrote: >> On Sat, Nov 24, 2012 at 1:53 PM, Gergely Kis >> 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 >>

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

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

On Sat, Nov 24, 2012 at 1:53 PM, Gergely Kis 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 i

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 wrote: > Hi, > > Yes, I saw that thre

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

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

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 t

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