From 0e2bb26240b785d4ca618cfbc042b13c613fa78f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 11 Mar 2019 13:52:21 +0100
Subject: Don't coqchk the test suite prerequisites

This causes the makefile to break due to dependencies when it fails,
and it's not worth adding a whole mess of code to catch the failure
for these files.
---
 test-suite/Makefile | 2 --
 1 file changed, 2 deletions(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6efd47afc2..ba591ede20 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -317,8 +317,6 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	    echo "    $<...correctly prepared" ; \
 	  fi; \
 	} > "$@"
-	@echo "CHECK     $<"
-	$(HIDE)$(coqchk) -norec TestSuite.$(shell basename $< .v) > $(shell dirname $<)/$(shell basename $< .v).chk.log 2>&1
 
 ssr: $(wildcard ssr/*.v:%.v=%.v.log)
 $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v)): %.v.log: %.v $(PREREQUISITELOG)
-- 
cgit v1.2.3