Re: Can't build external-widget.texi, old makeinfo?