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.
---
 Dockerfile.make | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Dockerfile.make')

diff --git a/Dockerfile.make b/Dockerfile.make
index 7972ad7..1a1dfc2 100644
--- a/Dockerfile.make
+++ b/Dockerfile.make
@@ -26,4 +26,5 @@ RUN ["/bin/bash", "--login", "-c", "set -x \
   && cd mathcomp \
   && make Makefile.coq \
   && make -f Makefile.coq -j ${NJOBS} all \
-  && make -f Makefile.coq install"]
+  && make -f Makefile.coq install \
+  && make test-suite"]
-- 
cgit v1.2.3