diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-10 17:12:15 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-11 14:58:15 +0200 |
| commit | 5525451a035e6faafa780c291efc2e5113637b70 (patch) | |
| tree | 430ee8cbff4ff901d91072eeb85271af64ccc86a /tools | |
| parent | b6d4575e39d32d276bed84ccb6b2b67a2e7bccb6 (diff) | |
Fix 5776 - `make` gives `ocamlfind: No such file or directory` on every execution
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 cfa552602..8f79f8a66 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -179,8 +179,6 @@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS) -CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib) - # FIXME This should be generated by Coq GRAMMARS:=grammar.cma ifeq ($(CAMLP4),camlp5) @@ -189,7 +187,12 @@ else CAMLP4EXTEND= endif +CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null) +ifeq (,$(CAMLLIB)) +PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.") +else PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' +endif ifneq (,$(TIMING)) TIMING_ARG=-time |