From 688c639f3e145989fa5c3e5f5af59a627e730ad7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 21 Jan 2005 17:30:06 +0000
Subject: Modification cible doc/coq.tex pour tenir des .mli qui n'existent pas
 toujours (mais nécessite une archive intègre sans .mli non déclarés)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6624 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile | 23 ++++++++---------------
 1 file changed, 8 insertions(+), 15 deletions(-)

diff --git a/Makefile b/Makefile
index c68f2748f9..3a8f99b266 100644
--- a/Makefile
+++ b/Makefile
@@ -1293,21 +1293,14 @@ install-latex:
 doc: doc/coq.tex
 	$(MAKE) -C doc coq.ps minicoq.dvi
 
-LPLIB = lib/doc.tex $(LIBREP:.cmo=.mli)
-LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli)
-LPLIBRARY = library/doc.tex $(LIBRARY:.cmo=.mli)
-LPPRETYPING = pretyping/doc.tex pretyping/rawterm.mli $(PRETYPING:.cmo=.mli)
-LPINTERP = $(INTERP:.cmo=.mli)
-LPPARSING = $(PARSING:.cmo=.mli) $(HIGHPARSING:.cmo=.mli)
-LPPROOFS = proofs/doc.tex $(PROOFS:.cmo=.mli)
-LPTACTICS = tactics/doc.tex $(TACTICS:.cmo=.mli) $(HIGHTACTICS:.cmo=.mli)
-LPTOPLEVEL = toplevel/doc.tex $(TOPLEVEL:.cmo=.mli)
-LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY) \
-	  $(LPPRETYPING) $(LPPROOFS) $(LPTACTICS) $(LPTOPLEVEL)
-
-doc/coq.tex: $(LPFILES)
-	ocamlweb -p "\usepackage{epsfig}" $(LPFILES) -o doc/coq.tex
-#	ocamlweb $(LPFILES) -o doc/coq.tex
+doc/coq.tex:
+	ocamlweb -p "\usepackage{epsfig}" \
+	doc/macros.tex 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
 
 clean::
 	rm -f doc/coq.tex
-- 
cgit v1.2.3