git switchover complete

[Tom Tromey]

I've switched to the new git repository.

You should now re-clone.  If you already have branches based on the
previous git repository, you will want to rebase them.

Please take care not to push branches referring to the previous git
branches into the new repository.

I've moved all the new commits from master over to the new repository.

Let me know if there are any problems.  And, let's all cross our fingers
and hope this is the last such switchover.  I realize it is a pain -- if
it's any consolation it is quite a pain for me as well, as I have to
re-rebase all my own branches...

Tom