[m-rev.] for review: Install stub mdb_doc if makeinfo/info are not available.

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

    Add a stub file.

    Copy the stub file if mdb_doc cannot be generated.

diff --git a/doc/Mmakefile b/doc/Mmakefile
index 1f347fd32..df33e3d18 100644
--- a/doc/Mmakefile
+++ b/doc/Mmakefile
@@ -227,6 +227,7 @@ mercury_library/index.html: library.texi_pp
 	# Warning: Unable to build mdb documentation.
 	# This is probably due to a missing `makeinfo' or `info'.
+	cp mdb_doc_stub.txt mdb_doc
 mdb_doc: generate_mdb_doc mercury_user_guide.info mdb_categories
diff --git a/doc/mdb_doc_stub.txt b/doc/mdb_doc_stub.txt
new file mode 100644
index 000000000..f30ce0721
--- /dev/null
+++ b/doc/mdb_doc_stub.txt
@@ -0,0 +1,6 @@
+document_category 100 no_mdb_doc
+Sorry, mdb help is not available.
+This is probably due to missing `makeinfo' or `info'
+when the Mercury system was installed.

More information about the reviews mailing list