aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar mrmr1993 <mr_1993@hotmail.co.uk>2018-03-03 11:00:50 +0000
committerGravatar mrmr1993 <mr_1993@hotmail.co.uk>2018-03-05 14:35:30 +0000
commit9d44eb55a515511e6d9bb2fa093b34a987753335 (patch)
tree9b6a7b058a7c9be3525dd66ca7fb4dbbc2cfc515
parent90dcc8ff89a495d18d319ecb6036f777e697089d (diff)
Tidy up ml-doc outut, give it a separate output directory
-rw-r--r--Makefile.doc7
1 files changed, 6 insertions, 1 deletions
diff --git a/Makefile.doc b/Makefile.doc
index 746ed1469..9325ef7e6 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -433,7 +433,12 @@ OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -
$(OCAMLDOC_MLLIBD)
ml-doc:
- $(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(DOCMLS)
+ $(SHOW)'OCAMLDOC -html'
+ $(HIDE)mkdir -p $(OCAMLDOCDIR)/html/implementation
+ $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) \
+ $(DOCMLS) -d $(OCAMLDOCDIR)/html/implementation -colorize-code \
+ -t "Coq mls documentation" \
+ -css-style ../style.css
parsing/parsing.dot : | parsing/parsing.mllib.d
$(OCAMLDOC_MLLIBD)