From d769a3d3c12adb4ac01c97eee94b41d8faf3a2f5 Mon Sep 17 00:00:00 2001 From: Jan Nieuwenhuizen Date: Sat, 21 Jul 2018 11:19:55 +0200 Subject: [PATCH] build: Fix for handling missing makeinfo. * configure (main): Update MAKEINFO. --- configure | 1 + 1 file changed, 1 insertion(+) diff --git a/configure b/configure index efc7d483..44c8f8b2 100755 --- 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 ""))