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

[Jesus Sanchez-Palencia]

2012/11/28 Adam Barth <abarth at 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