Replace git_coreteam.py with coreteam.sh

The script git_coreteam.py uses outdated gitstats information
from the web, while the new script uses the git shortlog from the
repository itself (with a little help of recently added .mailmap).