On 5 May 2018 at 13:33, Paul Eggert <eggert@cs.ucla.edu> 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.