diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-27 16:55:23 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-27 16:55:23 +0100 |
| commit | 11054617ada7fd2d9c31a6b5f13fe0633a34c0e6 (patch) | |
| tree | dbda5f71fe8ed6efece8fc51c737ee2f4787e0d6 /tools | |
| parent | 68061d8d464d0c62442675897c9c5f6db8d2b2e4 (diff) | |
| parent | 9fd736aaefc53943c1d5c81295d80b234469e0eb (diff) | |
Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 8f79f8a66..4ee6efec0 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -179,6 +179,9 @@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS) +# ocamldoc fails with unknown argument otherwise +CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) + # FIXME This should be generated by Coq GRAMMARS:=grammar.cma ifeq ($(CAMLP4),camlp5) @@ -407,12 +410,12 @@ mlihtml: $(MLIFILES:.mli=.cmi) $(SHOW)'CAMLDOC -d $@' $(HIDE)mkdir $@ || rm -rf $@/* $(HIDE)$(CAMLDOC) -html \ - -d $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES) + -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) all-mli.tex: $(MLIFILES:.mli=.cmi) $(SHOW)'CAMLDOC -latex $@' $(HIDE)$(CAMLDOC) -latex \ - -o $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES) + -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) gallina: $(GFILES) |