aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Jason Gross <jasongross9@gmail.com>2017-06-28 12:31:41 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-30 13:17:43 -0400
commitb55d44168ee39b0d9da8364238e716526ffcf920 (patch)
treea6e39f8a28a92718f44e7d6157ff8a41d4cc887d /tools
parent2a95acfe2892d982cda1fcd7c7a921c8e25f16d4 (diff)
Fix more potential quoting issues: COQBIN , COQLIB
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in15
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