Remove unnecessary file

Has been introduced in 9fdcbe7a, but
wrongly named (file name contains a space character). An updated version
has been added with the proper name in
1f554266. This makes the former file
obsolete, and it should be purged from the tree.