Removing auto-generated files from git index.
These files are already in the .gitignore file but might have been accidently included in #1495.

This should decrease the risk of including stray files in future PRs.

Checklist

• PR contains only changes related; no stray files, etc.
• README updated (where applicable)
• Tests written (where applicable)

Instead of submitting a new PR I believe you should amend your original PR commit as I doubt it will be merged that way.

Actually it was indeed merged, and it was not a PR from me :-)

Closing as this will be taken care by #1553.