[m-rev.] for review: Warn if missing makeinfo/info.

Peter Wang novalazy at gmail.com
Mon May 27 17:18:02 AEST 2019

    Add warning message at end if missing makeinfo/info.

diff --git a/configure.ac b/configure.ac
index bc56bdc55..a814aadfd 100644
--- a/configure.ac
+++ b/configure.ac
@@ -5714,5 +5714,14 @@ MERCURY_MSG(["You can make the install faster by installing fewer grades,"])
 MERCURY_MSG(["as shown by the fine-tuning section of the INSTALL file,"])
 MERCURY_MSG(["or by compiling the files of each grade in parallel,"])
 MERCURY_MSG(["which you can do via a command such as make PARALLEL=-j2 install."])
+if test -z "$MAKEINFO" -o -z "$INFO"
+    MERCURY_MSG(["WARNING: missing \`makeinfo' or \`info'."])
+    MERCURY_MSG(["They are necessary to generate documentation in all formats,"])
+    MERCURY_MSG(["as well as help text in the debugger."])
+    MERCURY_MSG("")

More information about the reviews mailing list