diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-08-17 12:15:03 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-08-31 17:00:09 +0200 |
| commit | 2d8cbd7d4e5397a0c47c4dba9cfccac16ab66228 (patch) | |
| tree | d1c4baa471b6de4d09dbd34be4698be6adb19d1a /Makefile.doc | |
| parent | 13fb8de9aff07e4346ca4bdc866507503e9be12e (diff) | |
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].
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 15 |
1 files changed, 7 insertions, 8 deletions
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 |