aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEnrico Tassi2020-09-10 15:06:33 +0200
committerGitHub2020-09-10 15:06:33 +0200
commitff61778018f5eff362a50e48e5b3fd30dec962d2 (patch)
tree7d20fd50e25f01219d1b961a9a298fb906b3a5c7
parent18edef73cdf0fb6671dbfb2e9d5829182a065919 (diff)
Update mathcomp/Makefile.test-suite.coq.local
Co-authored-by: Erik Martin-Dorel <erik@martin-dorel.org>
-rw-r--r--mathcomp/Makefile.test-suite.coq.local2
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/Makefile.test-suite.coq.local b/mathcomp/Makefile.test-suite.coq.local
index 119eff1..9db49c5 100644
--- a/mathcomp/Makefile.test-suite.coq.local
+++ b/mathcomp/Makefile.test-suite.coq.local
@@ -16,5 +16,5 @@ post-all:: $(OUTPUT_ARTIFACTS)
fi;\
done
-$(OUTPUT_ARTIFACTS): %.v.out.new: %.v all/all.vo
+$(OUTPUT_ARTIFACTS): %.v.out.new: %.v
$(COQC) $(COQFLAGS) $(COQLIBS) $< > $<.out.new