[bug#40815] gnu: Add metamath

[Nicolas Goaziou]

Hello,

elaexuotee@wilsonb.com writes:

>> 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.

The book looks like a related project to metamath, like advanced
documentation, not like a regular manual. I didn't read it, so it is
just a guess.

Anyway, I only suggested it as another option to consider. Feel free to
ignore it.

> 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?

I do. In any case, if you want to keep them, they need to start with two
semicolons, not a single one.

WDYT?

Regards,
-- 
Nicolas Goaziou