From a899bb7ef1d6a2c35b1b9a646dfeae332972f5f6 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Thu, 26 Sep 2019 09:48:48 +0200
Subject: Fix and improve the test suite and Makefile

- improve an error message produced by the `check_join` tactic,
- fix the build of the test suite: `make test-suite`, and
- add a new rule `only` to build a subset of MathComp.
---
 mathcomp/Make.test-suite | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 mathcomp/Make.test-suite

(limited to 'mathcomp/Make.test-suite')

diff --git a/mathcomp/Make.test-suite b/mathcomp/Make.test-suite
new file mode 100644
index 0000000..bca6ed9
--- /dev/null
+++ b/mathcomp/Make.test-suite
@@ -0,0 +1,7 @@
+test_suite/hierarchy_test.v
+
+-I .
+-R . mathcomp
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -ambiguous-paths
-- 
cgit v1.2.3