Packaged versions of the HTML format need to include any .txt files that
were generated by the use of the productionlist environment or the
\verbatiminput macro.
diff --git a/Doc/Makefile b/Doc/Makefile
index c9045ce..59938dd 100644
--- a/Doc/Makefile
+++ b/Doc/Makefile
@@ -349,18 +349,18 @@
html-$(RELEASE).tgz: html
(cd $(HTMLDIR); \
- tar cf - *.html */*.css */*.html */*.gif) \
+ tar cf - *.html */*.css */*.html */*.gif */*.txt) \
| gzip -9 >$@
html-$(RELEASE).tar.bz2: html
(cd $(HTMLDIR); \
- tar cf - *.html */*.css */*.html */*.gif) \
+ tar cf - *.html */*.css */*.html */*.gif */*.txt) \
| bzip2 -9 >$@
html-$(RELEASE).zip: html
rm -f $@
(cd $(HTMLDIR); \
- zip -q -9 ../$@ *.html */*.css */*.html */*.gif)
+ zip -q -9 ../$@ *.html */*.css */*.html */*.gif */*.txt)
# convenience targets: