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

[Adam Barth]

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