> Note the book could also go into another package, once texlive-amsfonts is
> fixed.

Interesting. Either way it's a similarly sized patch, so I'm curious why a
"metamath-doc" packages would be preferable to a "metamath:doc" output.

> Meanwhile, I think we can remove the comments in this one and apply it.
> 
> WDYT?

Sure. You intuition on what is best for the repo is certainly more honed than
mine. Would you mind sharing your reasoning for deleting the comments though?
Not sure I see why.

My thinking was this: want want a "doc" output if possible; the work of
creating that is already done; so we might as well make that work available.
Are you mostly trying to avoid comment clutter?

Either way, the patch I included here strips out the comments.

> I don't have enough knowledge to comment LaTeX packages. I suggest to
> submit them as separate issues. If still no one comments of them, I'll
> apply them later.

Great. I'll do that. Thanks.

Cheers!