|
| From: | Paul Eggert |
| Subject: | Re: master 7b1026c: * make-dist: Don't fail if building --without-makeinfo. |
| Date: | Sat, 5 May 2018 10:33:40 -0700 |
| User-agent: | Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.7.0 |
Eli Zaretskii wrote:
Yes. I think it makes more sense to try and then go ahead if production of Info files fails. It's not a strong opinion, though.
Although that would be OK ordinarily, a user who runs './make-dist --no-info' does not want info files in the tarball and my point was that make-dist should not try to build them in that case.
| [Prev in Thread] | Current Thread | [Next in Thread] |