GNU bug report logs - #40815
gnu: Add metamath

Previous Next

Full log

Message #44 received at 40815 <at> debbugs.gnu.org (full text, mbox):

From: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
To: elaexuotee <at> wilsonb.com
Cc: Jakub Kądziołka <kuba <at> kadziolka.net>,
 40815 <at> debbugs.gnu.org
Subject: Re: [bug#40815] gnu: Add metamath
Date: Sun, 28 Jun 2020 22:12:09 +0200

Hello,

elaexuotee <at> 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

Previous Next

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