aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile5
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 0e0840d71..8a8461cf4 100644
--- a/Makefile
+++ b/Makefile
@@ -36,8 +36,9 @@ OBJS=$(CONFIG) $(LIB) $(KERNEL)
world: $(OBJS)
-MLI=$(OBJS:.cmo=.mli)
-LPFILES=doc/macros.tex $(MLI)
+LPLIB = lib/doc.tex $(LIB:.cmo=.mli)
+LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli)
+LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL)
lp: doc/coq.ps
doc/coq.ps: doc/coq.tex
cd doc; make coq.ps