aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>1999-08-19 08:17:17 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>1999-08-19 08:17:17 +0000
commit10f4e87cca4f83700c9b6a8acffc081de66dc164 (patch)
tree71d963bff3495ecd124abc9466890f83d42577f0 /Makefile
parent2178b546a941803548bd2699a860086ad8f5f1d5 (diff)
mise en place programmation literaire (generation de doc/coq.tex)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile8
1 files changed, 8 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 0407fd12b..b11d9b0c7 100644
--- a/Makefile
+++ b/Makefile
@@ -35,6 +35,14 @@ OBJS=$(CONFIG) $(LIB) $(KERNEL)
world: $(OBJS)
+MLI=$(OBJS:.cmo=.mli)
+LPFILES=doc/macros.tex $(MLI)
+lp: doc/coq.ps
+doc/coq.ps: doc/coq.tex
+ cd doc; make coq.ps
+doc/coq.tex: $(LPFILES)
+ ocamlweb -o doc/coq.tex $(LPFILES)
+
# Default rules
.SUFFIXES: .ml .mli .cmo .cmi .cmx