Deploy Key and Mirroring for GitHub Repo

Ref: https://meta.trac.wordpress.org/ticket/633

git.develop is being mirrored by GitHub, but their mirror process only checks every few hours, which is way too slow to be useful. Instead, we want to replace it with a post-receive push.

To do that, we need a deployDeploy Launching code from a local development environment to the production web server, so that it's available to visitors. key created, per GitHub’s docs.

The private key needs to live on the git server, either in ssh agent, or with a reference in the ssh config file:

Host github.com
    IdentityFile ~/.ssh/id_rsa_github

The push command then needs to be added to the post-receive script.

git push -f --mirror git@github.com:WordPress/wordpress-develop.git

I’d like to get this done quickly, so we can get GitHubGitHub GitHub is a website that offers online implementation of git repositories that can can easily be shared, copied and modified by other developers. Public repositories are free to host, private repositories require a paid subscription. GitHub introduced the concept of the ‘pull request’ where code changes done in branches by contributors can be reviewed and discussed before being merged be the repository owner. https://github.com/ integrations up and running. Thanks!

#prio1