Should ‘./configure’ check for makeinfo?  ‘make’ will fail when makeinfo
isn’t installed.