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

[Peter Wang]

doc/mdb_doc_stub.txt:
    Add a stub file.

doc/Mmakefile
    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
 warn_no_mdb_doc:
 	# 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
 	./generate_mdb_doc
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.
+
+end
-- 
2.21.0