aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar mrmr1993 <mr_1993@hotmail.co.uk>2018-03-03 10:56:12 +0000
committerGravatar mrmr1993 <mr_1993@hotmail.co.uk>2018-03-05 14:35:30 +0000
commit90dcc8ff89a495d18d319ecb6036f777e697089d (patch)
tree9d6102df0448e0125a36aaea97f92e944e454e89
parent15331729aaab16678c2f7e29dd391f72df53d76e (diff)
Use computed deps to generate ml-doc and use implicit mli-doc deps
-rw-r--r--Makefile.doc9
1 files changed, 4 insertions, 5 deletions
diff --git a/Makefile.doc b/Makefile.doc
index 894ef9a99..746ed1469 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -387,10 +387,9 @@ install-doc-index-urls:
OCAMLDOCDIR=dev/ocamldoc
-DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \
- ./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \
- ./parsing/*.mli ./proofs/*.mli \
- ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli)
+DOCMLS=$(foreach lib,$(CORECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .ml, $($(lib))))
+
+DOCMLIS=$(wildcard $(addsuffix /*.mli, $(CORESRCDIRS)))
# Defining options to generate dependencies graphs
DOT=dot
@@ -434,7 +433,7 @@ OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -
$(OCAMLDOC_MLLIBD)
ml-doc:
- $(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES)
+ $(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(DOCMLS)
parsing/parsing.dot : | parsing/parsing.mllib.d
$(OCAMLDOC_MLLIBD)