There's already support for stripping comments as part of the make arxiv target, but we have \ignore{} too. We need to get rid of all the \ignore{}, too since they contain gods know what, and we don't need to be sharing old, stale text with the world.
There's already support for stripping comments as part of the
make arxiv
target, but we have \ignore{} too. We need to get rid of all the \ignore{}, too since they contain gods know what, and we don't need to be sharing old, stale text with the world.