Do not .gitignore doc/man/man5/*.5, which are already in Git.