From 7e591e38da21c87741f8873b0d6e4a7b598f75ec Mon Sep 17 00:00:00 2001
From: notin
Date: Thu, 27 Apr 2006 16:04:30 +0000
Subject: 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
---
 Makefile | 14 +-------------
 1 file changed, 1 insertion(+), 13 deletions(-)

(limited to 'Makefile')

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
 
-- 
cgit v1.2.3