build: Fix for handling missing makeinfo.
authorJan Nieuwenhuizen <janneke@gnu.org>
Sat, 21 Jul 2018 09:19:55 +0000 (11:19 +0200)
committerJan Nieuwenhuizen <janneke@gnu.org>
Sat, 21 Jul 2018 09:19:55 +0000 (11:19 +0200)
* configure (main): Update MAKEINFO.

configure

index efc7d4830c2df117602fe41b9639cdbddae1ec06..44c8f8b2ae82c5105d1f27acad8d175a24ab66d7 100755 (executable)
--- a/configure
+++ b/configure
@@ -355,6 +355,7 @@ Some influential environment variables:
           (stdout "CC:=~a\n" (or CC ""))
           (stdout "CC32:=~a\n" (or CC32 ""))
           (stdout "HELP2MAN:=~a\n" (or HELP2MAN ""))
+          (stdout "MAKEINFO:=~a\n" (or MAKEINFO ""))
           (stdout "TCC:=~a\n" (or TCC ""))
           (stdout "BLOOD_ELF:=~a\n" (or BLOOD_ELF ""))
           (stdout "MES_SEED:=~a\n" (or MES_SEED ""))