|
From: | Paul Eggert |
Subject: | Re: master 7b1026c: * make-dist: Don't fail if building --without-makeinfo. |
Date: | Fri, 4 May 2018 23:53:41 -0700 |
User-agent: | Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.7.0 |
Eli Zaretskii wrote:
So would adding a --no-info argument (as in the attached) be okay?I think it would. But maybe it will make even more sense to try building the Info files, and only make the failure to do it non-fatal with that switch specified, WDYT?
Unless you specify --no-update, make-dist already tries to build the info files. If that fails make-dist goes ahead anyway; perhaps it shouldn't.
[Prev in Thread] | Current Thread | [Next in Thread] |