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

[Noam Postavsky]

On 5 May 2018 at 02:56, Paul Eggert <address@hidden> wrote:
> Noam Postavsky wrote:
>>
>> So would adding a --no-info argument (as in the attached) be okay?
>
>
> If --no-info is given, please also change make-dist so that it does not
> invoke 'make --question info' or 'make info'.

I think Eli is suggesting the opposite, so I'll hold off on making any
changes until we decide where we're going.

> (Good catch in getting rid of that '[ -d info ]'.)

I can't really claim credit for that, since I was the one who added it ;)
(in the commit mentioned at the top of this thread)