dcb91cf0c0c9a20622feeb4e5e8104ffbc9fa8ec hacked around the biggest issue
this caused, but wasted a lot of CPU time and disk space It also still
included a lot of other unwanted files. This removes all of `doc/` except
the license, and also removes the server list.