chiark / gitweb /
dgit-repos-server: rename from dgit-repos-push-receiver