contributors.sh: filter common alternative name spellings

docs/THANKS-filter is a new filter file for converting contributor names
we get or have recorded in alternative formats to the one we already use
in THANKS. To help us show individual contributors using a single
presentation of their names.