aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tools/CoqMakefile.in2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 4ee6efec0c..87783350a2 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)