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

[Paul Eggert]

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.