From 261103b5bfd89335d028bf800af3f0a1ab1b70e5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 9 Mar 2010 15:13:00 +0000 Subject: New HTML documentation generator git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1286 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Makefile | 26 +++++++++++--------------- 1 file changed, 11 insertions(+), 15 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index d50a478..e3eb246 100644 --- a/Makefile +++ b/Makefile @@ -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 -- cgit v1.2.3