https://gitweb.torproject.org/ lists an "arma/tor" and an "arma/torspec", with no description string. And then a little bit lower it lists "user/arma/tor" and "user/arma/torspec". I'm looking at the gitolite-admin/conf/gitolite.conf file and it lists the user/arma/tor* ones but not the others. Where do the arma/tor* ones come from? Can we get rid of them? I kind of think we already got rid of them but they are back somehow. (Reported by ln5 who got snookered into thinking the arma/tor* ones were the ones he should use.)