aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
diff options
context:
space:
mode:
authorEnrico Tassi2020-09-11 16:35:14 +0200
committerEnrico Tassi2020-09-11 22:34:58 +0200
commita28ed91e0d3b2d03940c9b930ac516f0769f7e17 (patch)
treeb329b99544de0ab2ea2878cbe844485a12ef9baa /mathcomp
parentbcbf0850d771c889431fb8d3c073c41059268c05 (diff)
avoid rebuild
Diffstat (limited to 'mathcomp')
-rw-r--r--mathcomp/Makefile.common8
1 files changed, 7 insertions, 1 deletions
diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common
index b6b71ea..9759158 100644
--- a/mathcomp/Makefile.common
+++ b/mathcomp/Makefile.common
@@ -56,7 +56,13 @@ Makefile.coq: pre-makefile $(COQPROJECT) Makefile
# Test suite ---------------------------------------------------------
-test_suite/test_hierarchy_all.v: build
+ifneq "$(TEST_SKIP_BUILD)" ""
+TEST_DEP :=
+else
+TEST_DEP := build
+endif
+
+test_suite/test_hierarchy_all.v: $(TEST_DEP)
COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib all.all > test_suite/test_hierarchy_all.v
Makefile.test-suite.coq: test_suite/test_hierarchy_all.v