diff options
author | Jason Gross <jasongross9@gmail.com> | 2017-06-28 12:31:41 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-30 13:17:43 -0400 |
commit | b55d44168ee39b0d9da8364238e716526ffcf920 (patch) | |
tree | a6e39f8a28a92718f44e7d6157ff8a41d4cc887d /tools | |
parent | 2a95acfe2892d982cda1fcd7c7a921c8e25f16d4 (diff) |
Fix more potential quoting issues: COQBIN , COQLIB
Diffstat (limited to 'tools')
-rw-r--r-- | tools/CoqMakefile.in | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 3027bf92d..c4afc930a 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" @@ -177,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 @@ -632,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 |