don't install local HTML files

diff --git a/doc/all.mk b/doc/all.mk
index 45106f546c01d042d41a9eb4520b8bf097e694e8..c304ffa07c071cb69b3dd40489a48a10bf869f4e 100644 (file)
--- a/doc/all.mk
+++ b/doc/all.mk
@@ -123,7 +123,7 @@ DOC_FILES   := $(filter-out %~ %/all.mk %.gitignore doc/rfc/update.sh doc/develope
 #  We remove the "doc/" prefix, because the documentation files are
 #  installed into $(docdir)/foo, and not $(docdir)/doc/.
 #
-ALL_DOC_FILES  := $(patsubst doc/%,%,$(sort $(DOC_FILES) $(ADOC_FILES) $(HTML_FILES)))
+ALL_DOC_FILES  := $(patsubst doc/%,%,$(sort $(DOC_FILES) $(ADOC_FILES)
 
 #
 #  Install doc/FOO into $(R)$(docdir)/FOO