GNU bug report logs - #40815
gnu: Add metamath

Previous Next

Full log

View this message in rfc822 format

From: elaexuotee <at> wilsonb.com
To: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
Cc: Jakub Kądziołka <kuba <at> kadziolka.net>, 40815 <at> debbugs.gnu.org
Subject: [bug#40815] gnu: Add metamath
Date: Fri, 26 Jun 2020 17:46:22 +0900

[Message part 1 (text/plain, inline)]

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

[0001-gnu-Add-metamath.patch (text/x-patch, attachment)]

[signature.asc (application/pgp-signature, attachment)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.