Re: master 7b1026c: * make-dist: Don't fail if building --without-makeinfo.

[Noam Postavsky]

On 5 May 2018 at 13:33, Paul Eggert <address@hidden> wrote:
> 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.

Yes, I think I'd rather not see noise from error messages about it either.

v2-0001-make-dist-Add-no-info-option.patch
Description: Text Data