Suppression de l'entrée devdoc dans le Makefile principal et modification en conséquence du Makefile dans dev/doc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8750 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 13 deletions

diff --git a/Makefile b/Makefile
index a7b773347d..2ce9d466ba 100644
--- a/Makefile
+++ b/Makefile
@@ -1257,7 +1257,7 @@ install-latex:
 # Literate programming (with ocamlweb)
 ###########################################################################
 
-.PHONY: doc devdoc
+.PHONY: doc
 
 doc: glob.dump
 	(cd doc; make all)
@@ -1265,18 +1265,6 @@ doc: glob.dump
 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}" \
-	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 dev/doc/coq.tex
-
 clean::
 	rm -f doc/coq.tex