[bin/authors.sh] Make sure changed name doesn't resurface from git history

Issue codemirror#5037

Author: marijnh

bin/authors.sh

@@ -1,6 +1,6 @@
 # Combine existing list of authors with everyone known in git, sort, add header.
 tail --lines=+3 AUTHORS > AUTHORS.tmp
-git log --format='%aN' >> AUTHORS.tmp
+git log --format='%aN' | grep -v "Piët Delport" >> AUTHORS.tmp
 echo -e "List of CodeMirror contributors. Updated before every release.\n" > AUTHORS
 sort -u AUTHORS.tmp >> AUTHORS
 rm -f AUTHORS.tmp