diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 11:00:20 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 11:00:20 +0200 |
| commit | 296941dc97d53817cc58b4687ed99168e1dd33a9 (patch) | |
| tree | 0fe64507c184d3fc31c2c9219cf2068363c8e2c6 /Makefile.doc | |
| parent | 53fe81925820895e5657ec8c1d0389e96a0abc70 (diff) | |
| parent | 741943da6e42937f6d50db9c920a40073160eebc (diff) | |
Merge PR #979: Fix install-doc target and other gitlab failures
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 3f8ae3680..0c3b70149 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 |