Merge pull request #16542 from JGaunt/patch-3
authorMatthew Wire <mjw@mjwconsult.co.uk>
Fri, 14 Feb 2020 19:18:02 +0000 (19:18 +0000)
committerGitHub <noreply@github.com>
Fri, 14 Feb 2020 19:18:02 +0000 (19:18 +0000)
Update CONTRIBUTORS.txt


Trivial merge