diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-07-03 16:44:21 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-08-02 16:47:54 +0200 |
| commit | 8995d0857277019b54c24672439d3e19b2fcb5af (patch) | |
| tree | 8f35256f93be58008cb1effce4d4f1954b962250 /Makefile.doc | |
| parent | 1f46ff6db53c2ca471d9ea067d0824755b2f34da (diff) | |
Makefile.doc: implement serve-refman-8080 target
We make it so that, by default, the HTML reference manual looks
like the one published online (same .css) and we provide a target
to serve it locally (requires python).
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/Makefile.doc b/Makefile.doc index 6a81b292e..1fed4ee7b 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -36,7 +36,7 @@ HEVEA:=hevea HACHA:=hacha HEVEAOPTS:=-fix -exec xxdate.exe HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea -HTMLSTYLE:=simple +HTMLSTYLE:=coqremote export TEXINPUTS:=$(HEVEALIB): ifdef COQDOC_NOBOOT COQTEXOPTS:=-n 72 -sl -small @@ -216,7 +216,15 @@ doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ (cd doc/refman/html; $(HACHA) -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html) $(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html @touch $(INDEXES) - -$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html + (cd doc/common/styles/html/$(HTMLSTYLE);\ + for f in `find . -name \*.css`; do \ + install -m 644 -D $$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;\ @@ -479,6 +487,12 @@ $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex $(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex) $(HIDE)(cd doc/tools/; show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log) +########################################################################### +# local web server +########################################################################### + +serve-refman-8080: refman + cd doc/refman/html; python3 -m http.server 8080 # For emacs: # Local Variables: |