aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authornotin2006-03-14 15:01:00 +0000
committernotin2006-03-14 15:01:00 +0000
commitf548bcddd7aca88889978c092747e4427017cd43 (patch)
tree8dbfc2f39774a0dbfd49b9ad1e978a632f1391c1 /Makefile
parentf31923c002943eebd7601871658cd636f7f2de4e (diff)
r8637@thot: notin | 2006-03-14 16:00:49 +0100
- intégration de doc dans le Makefile principal - correction d'une incompatibilité avec Tetex 3.0 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8626 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile18
1 files changed, 12 insertions, 6 deletions
diff --git a/Makefile b/Makefile
index 6edd5ca47d..45a91e1e00 100644
--- a/Makefile
+++ b/Makefile
@@ -1240,19 +1240,25 @@ install-latex:
# Literate programming (with ocamlweb)
###########################################################################
-.PHONY: doc
+.PHONY: doc devdoc
-doc: doc/coq.tex
- $(MAKE) -C doc coq.ps minicoq.dvi
+doc: coq
+ (cd doc; make all)
-doc/coq.tex:
+clean::
+ (cd doc; make clean)
+
+devdoc: dev/doc/coq.tex
+ $(MAKE) -C dev/doc coq.ps minicoq.dvi
+
+dev/doc/coq.tex:
ocamlweb -p "\usepackage{epsfig}" \
- doc/macros.tex doc/intro.tex \
+ dev/doc/macros.tex dev/doc/intro.tex \
lib/{doc.tex,*.mli} kernel/{doc.tex,*.mli} library/{doc.tex,*.mli} \
pretyping/{doc.tex,*.mli} interp/{doc.tex,*.mli} \
parsing/{doc.tex,*.mli} proofs/{doc.tex,*.mli} \
tactics/{doc.tex,*.mli} toplevel/{doc.tex,*.mli} \
- -o doc/coq.tex
+ -o dev/doc/coq.tex
clean::
rm -f doc/coq.tex