Rename Operation section to Services
While writing a roadmap for the next 12 months of metrics team work it occurred to us that "Operation" as title might be misunderstood as everything around operating our services. But what we really want to include there are services that we provide that are related to operating the Tor network. It seemed like "Services" might be a better word here, because what we provide there are services.
However, I wonder if "Services" would still fit into the other categories then. We do provide services, but we don't provide development or research but instead information about development and information about research. Ideally, we'd find consistent names for these five or six (including About) categories.
Another concern that just came to mind: if we rename the category, we'll have to rename the web page from
/services.html and install redirects. Not impossible, but we should be sure that we want to do it and not undo it shortly after.
iwakeh and irl, what do you think, should we rename it? And what do you think about the concerns above? Should we also ask the UX people? Or should we simply keep this unchanged for the moment?