aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/Makefile.common
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/Makefile.common')
-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