aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/Makefile
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-24 19:13:30 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-25 11:19:08 +0200
commit3930c586507bfb3b80297d7a2fdbbc6049aa509b (patch)
treed6fa4c001548134886554e660c6eb58df3ef8020 /test-suite/Makefile
parentb6725a2d0077239e51385a62a526ab9465eea26d (diff)
Updating the documentation and the toolchain w.r.t. the change in -compile.
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile6
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index d2466250a..39c36d541 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -208,7 +208,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(coqc) "$*" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R != 0 ]; then \
echo $(log_failure); \
echo " $<...could not be prepared" ; \
@@ -238,7 +238,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(coqc) "$*" $(call get_coq_prog_args,"$<") -async-proofs on \
+ $(coqc) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \
-async-proofs-private-flags fallback-to-lazy-if-marshal-error=no,fallback-to-lazy-if-slave-dies=no \
$$opts 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
@@ -352,7 +352,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v
# Additionnal dependencies for module tests
$(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo
modules/%.vo: modules/%.v
- $(HIDE)$(coqtop) -R modules Mods -compile $(<:.v=)
+ $(HIDE)$(coqtop) -R modules Mods -compile $<
#######################################################################
# Miscellaneous tests