Michal Čihař - Migrating code to github

Migrating code to github

As you might have noticed from my previous posts, we've moved phpMyAdmin code to github. Now I'm going to describe some things which might be useful for you if you are about do to similar switch.

While using git, moving to another hosting provider should be pretty straightforward. Just add another remote, push code there and it should be done. On the other side you probably have dozens of things in your infrastructure which you need to adjust. So the first thing to do is write down what all services are connected to your current git repositories. Let me name some which might be worth checking:

  • continuous integration server
  • snapshots generating
  • demo server (in case you're providing something like we do)
  • commit notifications
  • various statistics services such as cia.vc
  • website generating
  • references in wiki, website and documetation

Once you think you have remembered all important things (the less important will probably show up anyway, but majority of things should work), you're ready to make the move.

I've decided to make the move in few steps. First push all data to new location, what can take some time. I'll get in more details to that later. In the same time I asked all contributors to give me their login information, so that I can allow them access to new repositories. Once all recently active developers were migrated, it was time to push all remaining commits to new git repositories and make the switch for real.

Pushing git repo to another location, should be pretty easy. On the other side if you have many branches, it get's slightly more complex, I've ended up with following shell snippet (pushing all branches present in origin to github remote):

git branch -r | grep origin/ | grep -v HEAD | sed 's@.*/@@' | while read b ; do git checkout $b ; git push github $b:$b ; done

Please ensure that you check output of this, because you may hit network problems somewhere in the middle and you end up with few branches than you expect. As the code is pretty much idempotent, you can safely run it several times until there is nothing to push. You should also push all tags to new location:

git push --tags github

Okay, we've all data on right place, so let's switch all our users to new location:

git remote set-url origin git@github.com:phpmyadmin/phpmyadmin.git # read/write
git remote set-url origin git://github.com/phpmyadmin/phpmyadmin.git # read only

Of course everybody has to do this manually.

Next good thing is to let people know when they are using wrong repo (which will stay there for some time). Unfortunately there is AFAIK no way to warn them on pull, so let's warn at least on push:

$ cat > hooks/update
#!/bin/sh
echo "phpMyAdmin git repositories have moved to https://github.com/phpmyadmin"
exit 1

I think this is pretty much all. You can find some more bits in our Git migration wiki page.

PS: Thanks to github for offering us hosting and sorry for breaking their branch displaying page by too many divergent branches.

Comments

Anonymous wrote on Feb. 8, 2012, 5:21 p.m.

You could warn users who pull from the old repository by adding a new branch named "phpmyadmin-repository-has-moved-to-github-slash-phpmyadmin", and putting a README file (and nothing else) in that branch. Anyone who pulls will see the notice of a new branch with an odd name that stands out.

wrote on Feb. 8, 2012, 6:29 p.m.

The easy way to mirror a git repo is to first make a new bare clone, and then push from that to the remote using --mirror. As in something like:

git clone --bare git://orig/foo.git
cd foo.git
git push --mirror ssh://dest/foo.git

wrote on Feb. 9, 2012, 11:55 a.m.

Well that's an option, though many people running some scripts won't notice this.

In the end I've decided to rename the repositories, so that everybody gets a failure and will hopefully start to look for reasons of the failure on our website.

wrote on Feb. 9, 2012, 4:21 p.m.

@Guillem: I thought there must be something like that, but did not find this nice solution. Thanks for the tip!