aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Ralf Jung <post@ralfj.de>2017-11-29 12:05:01 +0100
committerGravatar Ralf Jung <post@ralfj.de>2017-11-29 12:05:01 +0100
commitbbe7b785787ff3f13e5c2809a67241981b06e1db (patch)
treefbee2b762fc6404793cf2b4d79acb4868cb216db /tools
parent1207d5d018436e70a2ee386cb5644493c02cd983 (diff)
coq_makefile: pass filenames to coqchk
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 4ee6efec0..87783350a 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -392,7 +392,7 @@ checkproofs:
.PHONY: checkproofs
validate: $(VOFILES)
- $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=))
+ $(TIMER) $(COQCHK) $(COQCHKFLAGS) $^
.PHONY: validate
only: $(TGTS)