diff options
| author | Gaëtan Gilbert | 2017-11-24 14:25:20 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-11-24 14:27:55 +0100 |
| commit | 9fd736aaefc53943c1d5c81295d80b234469e0eb (patch) | |
| tree | 57582eb1057b1101cd789eb8d5ba2c4051f19abd /tools | |
| parent | f9b3414888aebd1186f53c46d737536670171ab6 (diff) | |
Fix coq-makefile ocamldoc call when configured with -annotate.
Fixes #6120.
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 8f79f8a669..4ee6efec0c 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) |