aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-07-31 14:24:11 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-08-29 17:39:41 +0200
commit028de158153de94adfcb9d1e995259d833968951 (patch)
tree0f02a6c03094971a3c095795e6a190618e470d45 /Makefile.doc
parentcc58638a8d33084c5c9f85ab4d536307da2d7929 (diff)
[general] Merge parsing with highparsing, put toplevel at the top of the linking chain.
Diffstat (limited to 'Makefile.doc')
-rw-r--r--Makefile.doc2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.doc b/Makefile.doc
index dd7717359..3f8ae3680 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -470,7 +470,7 @@ OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -
ml-doc:
$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES)
-parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d
+parsing/parsing.dot : | parsing/parsing.mllib.d
$(OCAMLDOC_MLLIBD)
grammar/grammar.dot : | grammar/grammar.mllib.d