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