diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-03-19 09:53:21 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-03-19 09:53:21 +0000 |
commit | 68881dcdf8be4c4ee8368574cf20cd2a38d383f9 (patch) | |
tree | 1f2e65c6a515768567f1254c98c2880b605828d1 /Makefile | |
parent | 22d8a1d40e38d1ca15d16fdc0aafca8d6228ecae (diff) |
Revu removeproof
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 9 |
1 files changed, 8 insertions, 1 deletions
@@ -74,7 +74,7 @@ all: $(MAKE) -C extraction $(MAKE) -C runtime -documentation: +documentation: doc/removeproofs @ln -f $(FILES) doc/ @mkdir -p doc/html cd doc; $(COQDOC) --html -d html \ @@ -83,6 +83,12 @@ documentation: cp doc/coqdoc.css doc/html/coqdoc.css doc/removeproofs doc/html/*.html +doc/removeproofs: doc/removeproofs.ml + ocamlopt -o doc/removeproofs doc/removeproofs.ml + +doc/removeproofs.ml: doc/removeproofs.mll + ocamllex doc/removeproofs.mll + latexdoc: cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES) @@ -103,6 +109,7 @@ install: clean: rm -f */*.vo *~ */*~ rm -rf doc/html doc/*.glob + rm -f doc/removeproofs.ml doc/removeproofs $(MAKE) -C extraction clean $(MAKE) -C runtime clean $(MAKE) -C test/cminor clean |