diff options
| author | herbelin | 2005-01-21 17:30:06 +0000 |
|---|---|---|
| committer | herbelin | 2005-01-21 17:30:06 +0000 |
| commit | 688c639f3e145989fa5c3e5f5af59a627e730ad7 (patch) | |
| tree | 79ba675fabd68f605fbd28ace76a24c3be4c9ced | |
| parent | 43795b5e6a5280b20201f3b6cd8fb7fe80491e43 (diff) | |
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
| -rw-r--r-- | Makefile | 23 |
1 files changed, 8 insertions, 15 deletions
@@ -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 |