diff options
| author | Maxime Dénès | 2017-07-05 09:41:02 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-05 09:41:02 +0200 |
| commit | 734d152ae1faf5feb427b978badc6ed0c95f4d5f (patch) | |
| tree | acea9659580478f6c3768a73c3f311418fc4a686 /tools | |
| parent | fb025512f4168c0a0f316458163822e831b51f43 (diff) | |
| parent | b55d44168ee39b0d9da8364238e716526ffcf920 (diff) | |
Merge PR #840: Quote $(OCAMLFIND) in CoqMakefile.in for Windows
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 38 |
1 files changed, 20 insertions, 18 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7b01c1b663..c4afc930a7 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -66,6 +66,7 @@ STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" # Coq binaries COQC ?= "$(COQBIN)coqc" +COQTOP ?= "$(COQBIN)coqtop" COQCHK ?= "$(COQBIN)coqchk" COQDEP ?= "$(COQBIN)coqdep" GALLINA ?= "$(COQBIN)gallina" @@ -73,11 +74,12 @@ COQDOC ?= "$(COQBIN)coqdoc" COQMKTOP ?= "$(COQBIN)coqmktop" # OCaml binaries -CAMLC ?= $(OCAMLFIND) ocamlc -c -rectypes -thread -CAMLOPTC ?= $(OCAMLFIND) opt -c -rectypes -thread -CAMLLINK ?= $(OCAMLFIND) ocamlc -rectypes -thread -CAMLOPTLINK ?= $(OCAMLFIND) opt -rectypes -thread -CAMLDEP ?= $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack +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 DESTDIR ?= @@ -139,7 +141,7 @@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) -CAMLLIB:=$(shell $(OCAMLFIND) printconf stdlib) +CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib) # FIXME This should be generated by Coq GRAMMARS:=grammar.cma @@ -149,7 +151,7 @@ else CAMLP4EXTEND= endif -PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' +PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" compat5.cmo $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' COQLIBINSTALL = $(COQLIB)user-contrib COQDOCINSTALL = $(DOCDIR)user-contrib @@ -176,7 +178,7 @@ ALLSRCFILES := \ # helpers vo_to_obj = $(addsuffix .o,\ $(filter-out Warning: Error:,\ - $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1)))) + $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) strip_dotslash = $(patsubst ./%,%,$(1)) VO = vo @@ -306,14 +308,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) @@ -631,14 +633,14 @@ printenv:: .merlin: $(SHOW)'FILL .merlin' $(HIDE)echo 'FLG -rectypes' > .merlin - $(HIDE)echo "B $(COQLIB)" >> .merlin - $(HIDE)echo "S $(COQLIB)" >> .merlin + $(HIDE)echo 'B $(COQLIB)' >> .merlin + $(HIDE)echo 'S $(COQLIB)' >> .merlin $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo "B $(COQLIB)$(d)" >> .merlin;) + echo 'B $(COQLIB)$(d)' >> .merlin;) $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo "S $(COQLIB)$(d)" >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo "B $(d)" >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo "S $(d)" >> .merlin;) + echo 'S $(COQLIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" .PHONY: merlin |