From 76ab524320e3d4c006c6c94372e0cfda2b62c76e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 22 Oct 2020 15:30:30 +0200
Subject: Build all_stdlib.v in test suite makefile

instead of recursive make
---
 Makefile.build | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index 526a8c5831..b307bde5df 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -603,7 +603,7 @@ $(CSDPCERTBYTE): $(CSDPCERTCMO)
 # tests
 ###########################################################################
 
-.PHONY: validate check test-suite $(ALLSTDLIB).v
+.PHONY: validate check test-suite
 
 VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -coqlib .
 
@@ -611,15 +611,11 @@ validate: $(CHICKEN) | $(ALLVO:.$(VO)=.vo)
 	$(SHOW)'COQCHK <theories & plugins>'
 	$(HIDE)$(CHICKEN) $(VALIDOPTS) $(ALLVO)
 
-$(ALLSTDLIB).v:
-	$(SHOW)'MAKE $(notdir $@)'
-	$(HIDE)echo "Require $(ALLMODS)." > $@
-
 MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE)
 
 check: validate test-suite
 
-test-suite: world byte $(ALLSTDLIB).v
+test-suite: world byte
 	$(MAKE) $(MAKE_TSOPTS) clean
 	$(MAKE) $(MAKE_TSOPTS) all
 
-- 
cgit v1.2.3