Corrupted ports.tar file?

[Dave Horsfall]

On Tue, 12 Apr 2022, Ryan Schmidt wrote:

> > I did run that first; apologies for not mentioning it (there were no 
> > issues).
> 
> I think you did mention it. I was suggesting you run it again, in case 
> somehow the server files were in a weird state the last time you 
> selfupdated. There was some intermittent network problem affecting the 
> server that generates the ports.tar file a few days ago, and again 
> today; although I thought our rsync updates happened pretty much 
> atomically, maybe it was possible for a set of files to be published 
> briefly that was not correct.

Sorry; my mistake.  I ran it again, and no problems; boy, do I hate these 
heisenbugs :-(

Many thanks.

-- Dave