diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-09 15:13:00 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-09 15:13:00 +0000 |
| commit | 261103b5bfd89335d028bf800af3f0a1ab1b70e5 (patch) | |
| tree | 8777745c993ce221a859763328ef2106390d867c /Makefile | |
| parent | a24cfb086163ab359735392340acfe03e133be64 (diff) | |
New HTML documentation generator
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1286 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 26 |
1 files changed, 11 insertions, 15 deletions
@@ -110,22 +110,18 @@ all: $(MAKE) ccomp $(MAKE) runtime -documentation: doc/removeproofs documentation-link - @mkdir -p doc/html - cd doc; $(COQDOC) --html -d html \ - $(FILES:%.v=--glob-from %.glob) $(FILES) - @cd doc; rm -f $(FILES) - cp doc/coqdoc.css doc/html/coqdoc.css - doc/removeproofs doc/html/*.html +documentation: doc/coq2html $(FILES) + mkdir -p doc/html + rm -f doc/html/*.html + doc/coq2html -o 'doc/html/%.html' doc/*.glob \ + $(filter-out doc/coq2html, $^) + cp doc/coq2html.css doc/coq2html.js doc/html/ -documentation-link: $(FILES) - @ln -f $^ doc/ +doc/coq2html: doc/coq2html.ml + ocamlopt -o doc/coq2html str.cmxa doc/coq2html.ml -doc/removeproofs: doc/removeproofs.ml - ocamlopt -o doc/removeproofs doc/removeproofs.ml - -doc/removeproofs.ml: doc/removeproofs.mll - ocamllex doc/removeproofs.mll +doc/coq2html.ml: doc/coq2html.mll + ocamllex doc/coq2html.mll latexdoc: cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES) @@ -163,7 +159,7 @@ clean: rm -f ccomp ccomp.byte rm -rf _build rm -rf doc/html doc/*.glob - rm -f doc/removeproofs.ml doc/removeproofs + rm -f doc/coq2html.ml doc/coq2html rm -f driver/Configuration.ml rm -f extraction/*.ml extraction/*.mli $(MAKE) -C runtime clean |