It can be regenerated if needed (and added to .gitignore I hope).
At this point, it's not useful. It actually hits us in "git grep"
when we look for code.
Signed-off-by: Alessandro Rubini <rubini@gnudd.com>