2017-06-25 00:49:30 UTC
scripts for generating those lists. The scripts seem to have been
devised with a specific purpose in mind, which is great, I create
scripts all the time. But without some general purpose I don't think
it's a good idea to keep these scripts in Git. Likewise the output was
useful in some context, which is great, but, again, not something to
keep in Git.
Looking at the Git log for these files (via git log -- doc/misc) shows
that no further work has been done with these files since they were
committed many years ago.
In the interest of reducing clutter, I'd like to remove all these files.
I wonder if anyone is opposed to that.
PS. Here are the files in question.