GitHub migration complete

[Chris Jones]

On 31/10/16 09:49, Clemens Lang wrote:
> Hi,
>
> On Mon, Oct 31, 2016 at 10:18:42AM +0100, René J.  V. Bertin wrote:
>> 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...
>
> Just as with Subversion, the answer is no. Remember that the PortIndex
> is specific to the macOS version you are running, so a server-generated
> PortIndex could only generate all of them into different files.
>
> Additionally, git does not preserve timestamps from the repository on
> checkout, so you might actually end up re-generating the index locally
> anyway.

After the initial checkout, when the first time generation of the index 
does take a short while, subsequent updates are from my perspective fast 
enough that this is not something to worry about. (I personally actually 
prefer to be generating it myself anyway).

Chris