GitHub migration complete

[René J. V. Bertin]

Clemens Lang wrote:

> If your question is not yet answered, ask on the mailing lists so it can
> be added.

I may have overlooked this, but does github have any provisions that would allow 
the PortIndex files to be generated on the server and served with the actual repo 
contents? That would probably give a very significant reduction in the resources 
spent collectively to regenerate those files...

R.