summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-03-19 09:53:21 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-03-19 09:53:21 +0000
commit68881dcdf8be4c4ee8368574cf20cd2a38d383f9 (patch)
tree1f2e65c6a515768567f1254c98c2880b605828d1 /Makefile
parent22d8a1d40e38d1ca15d16fdc0aafca8d6228ecae (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--Makefile9
1 files changed, 8 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index afadd77..58d494c 100644
--- a/Makefile
+++ b/Makefile
@@ -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