GitLab

We don't call the directory authorities "DirServers" much these days. The name dates back to when there was just one server in the whole network, I think, and everything else was a mere cache. It would probably make way more sense to rename the option. We should keep the old one as an alias, though, so things don't break.