On Fri, Jul 15, 2016 at 04:10:40PM +0200, Ludovic Courtès wrote: > Having several URLs pointing to the same server would be similarly > inefficient.
Indeed. So we could modify this again if we ever have distinct mirror machines, not just distinct names. Andreas