aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Jason Gross <jasongross9@gmail.com>2017-06-28 12:20:47 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-30 13:17:43 -0400
commit05db464aefe90ff69ea69d5ce7c4775c6a7f218f (patch)
tree9cd099b80bb2ff48f4e7b39ed4abcb4d39f3aac0 /tools
parente7bc719df55907b00b04f9fa2d45dba2da838360 (diff)
Create a variable for CAMLDOC in CoqMakefile.in
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in9
1 files changed, 5 insertions, 4 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 29e2a89e3..4f967e633 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -77,6 +77,7 @@ CAMLC ?= "$(OCAMLFIND)" ocamlc -c -rectypes -thread
CAMLOPTC ?= "$(OCAMLFIND)" opt -c -rectypes -thread
CAMLLINK ?= "$(OCAMLFIND)" ocamlc -rectypes -thread
CAMLOPTLINK ?= "$(OCAMLFIND)" opt -rectypes -thread
+CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -rectypes
CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
# DESTDIR is prepended to all installation paths
@@ -306,14 +307,14 @@ html: $(GLOBFILES) $(VFILES)
-toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES)
mlihtml: $(MLIFILES:.mli=.cmi)
- $(SHOW)'OCAMLDOC -d $@'
+ $(SHOW)'CAMLDOC -d $@'
$(HIDE)mkdir $@ || rm -rf $@/*
- $(HIDE)"$(OCAMLFIND)" ocamldoc -html -rectypes \
+ $(HIDE)$(CAMLDOC) -html \
-d $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES)
all-mli.tex: $(MLIFILES:.mli=.cmi)
- $(SHOW)'OCAMLDOC -latex $@'
- "$(OCAMLFIND)" ocamldoc -latex -rectypes \
+ $(SHOW)'CAMLDOC -latex $@'
+ $(HIDE)$(CAMLDOC) -latex \
-o $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES)
gallina: $(GFILES)