This is very handy when updating the RELEASE-NOTES as then we sometimes
have names added manually in the existing list and we use this script to
update the set.
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.
