[wp-meta] [Making WordPress.org] #633: Add sync for develop.git.wordpress.org with Github

[Making WordPress.org]

#633: Add sync for develop.git.wordpress.org with Github
-----------------------------+------------------
 Reporter:  jorbin           |       Owner:
     Type:  enhancement      |      Status:  new
 Priority:  normal           |   Milestone:
Component:  Version Control  |  Resolution:
 Keywords:                   |
-----------------------------+------------------

Comment (by dd32):

 I'm 90% certain that the `post-receive` hook mention on there is so that
 you could run something like `git pull origin master; git push` (I can't
 remember the exact commands..), which is what we were avoiding by using
 the Github mirror functionality.

 By using the mirror functionality it appears - although I haven't asked
 anyone, that this means it's basically on a recurring job to update it
 occasionally. That isn't going to work for us and our want for
 instantaneous pushes, so we're going to need to handle it manually with a
 `post-receive` hook I expect.
 The ideal option would be for there to be a webhook we can ping to trigger
 an update - if we want to reduce the amount of code in play on our side.

 Lets avoid setting up Travis until we have this figured out, Just to
 reduce the usage of the repo until we're sure.

 Also; What do we need to do to get all commits referencing the author? Ie.
 compare
 https://github.com/WordPress/WordPress/commit/3a0e61e680c9fd93440dd80e280991e544ff7ad7
 to https://github.com/WordPress/wordpress-
 develop/commit/07b8be117762c804d24c611a518c9aec0c4173ee

--
Ticket URL: <https://meta.trac.wordpress.org/ticket/633#comment:17>
Making WordPress.org <https://meta.trac.wordpress.org/>
Making WordPress.org