diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-12 11:48:51 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-12 11:48:51 +0200 |
| commit | 449ee4682abf27f04982d23ad6f5f6470953a086 (patch) | |
| tree | 21aa46745885b1f5072d242e51a7bff77678bd72 | |
| parent | 354ee7d67efda8624cb46e942f2a41211cadd030 (diff) | |
| parent | 5525451a035e6faafa780c291efc2e5113637b70 (diff) | |
Merge PR #1144: Fix 5776 - `make` gives `ocamlfind: No such file or directory` on every execution
| -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 |