doc: html: fix build with parallel make

* doc/local.mk (html-local): Add html files to prerequisites so they are
generated before 'sed' is invoked.  Also interate over the already
populated $(HTMLS) to be more general (to multiple html files),
and more portable (to non GNU make).

diff --git a/doc/local.mk b/doc/local.mk
index da5d21240d6f9ff959bbb5f283706a43545a9743..1287fca857a7798f3774eb286e0efd8cd752ae18 100644 (file)
--- a/doc/local.mk
+++ b/doc/local.mk
@@ -135,9 +135,9 @@ check-local: check-texinfo
 # Post-process generated HTML to clean up anchor IDs
 _sed_anchor_cleanup = \
   -e '/id=.*_002doption/ { s/id="\([^"]*\)_002doption/id="\1/g; s/_002d/-/g; }'
-html-local:
-       $(AM_V_GEN)htmlfile=$(info_TEXINFOS:.texi=.html); \
-       sed $(_sed_anchor_cleanup) $$htmlfile > $$htmlfile-t \
-         && mv $$htmlfile-t $$htmlfile
+html-local: $(HTMLS)
+       $(AM_V_GEN)for htmlfile in $(HTMLS); do \
+         sed $(_sed_anchor_cleanup) $$htmlfile > $$htmlfile-t \
+           && mv $$htmlfile-t $$htmlfile; done
 
 .PHONY: html-local