Ignore districts for now

They are not yet implemented on the map and would only clutter
the map.

scripts/geojson/maps/fetch_city_outlines.sh

@@ -9,6 +9,9 @@ for entry in $data; do
 	name=`echo "$entry" | sed -n 's/\s*\([^|]\+\).*/\1/p' | sed 's/ $//'`
 	type=`echo "$entry" | sed -n 's/\s*\([^|]\+\)||\s*\([^|]\+\).*/\2/p' | sed 's/ $//'`
 	coord=`echo "$entry" | sed -n 's/.*||\s*\([^|]\+\).*/\1/p'`
+	if [[ "$type" == "district" ]]; then
+		continue;
+	fi
 	if [[ "$name" != "" && "$coord" != "" ]]; then
 		echo "{ \"type\": \"Feature\",
 	\"geometry\": {