From 2d8cbd7d4e5397a0c47c4dba9cfccac16ab66228 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 17 Aug 2017 12:15:03 +0200 Subject: Fix install-doc target Since 8995d0857277019b54c24672439d3e19b2fcb5af [make doc] puts css files in subdirectories of doc/refman/html. These subdirectories cause a failure when doing [install doc/refman/html/* target]. --- Makefile.doc | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'Makefile.doc') diff --git a/Makefile.doc b/Makefile.doc index dd7717359..bc5dfa391 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -218,13 +218,9 @@ doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ @touch $(INDEXES) (cd doc/common/styles/html/$(HTMLSTYLE);\ for f in `find . -name \*.css`; do \ - install -m 644 -D $$f ../../../../refman/html/$$f;\ + $(MKDIR) $$(dirname ../../../../refman/html/$$f);\ + $(INSTALLLIB) $$f ../../../../refman/html/$$f;\ done) - (cd doc/common/styles/html/$(HTMLSTYLE);\ - for f in `find . -name coqdoc.css -o -name style.css`; do \ - install -m 644 -D $$f ../../../../refman/html/;\ - done) - install -m 644 doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html refman-quick: (cd doc/refman;\ @@ -391,8 +387,11 @@ install-doc-meta: install-doc-html: $(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib faq) - $(INSTALLLIB) doc/refman/html/* $(FULLDOCDIR)/html/refman - $(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib + (for f in `cd doc/refman/html; find . -type f`; do \ + $(MKDIR) $$(dirname $(FULLDOCDIR)/html/refman/$$f);\ + $(INSTALLLIB) doc/refman/html/$$f $(FULLDOCDIR)/html/refman/$$f;\ + done) + $(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib $(INSTALLLIB) doc/RecTutorial/RecTutorial.html $(FULLDOCDIR)/html/RecTutorial.html $(INSTALLLIB) doc/faq/html/* $(FULLDOCDIR)/html/faq $(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html -- cgit v1.2.3