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
---
 test-suite/Makefile | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 279f32c903..cee54f691c 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -144,6 +144,7 @@ bugs: $(BUGS)
 clean:
 	rm -f trace .csdp.cache .nia.cache .lia.cache output/MExtraction.out
 	rm -f vos/Makefile vos/Makefile.conf
+	rm -f misc/universes/all_stdlib.v
 	$(SHOW) 'RM        <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>'
 	$(HIDE)find . \( \
 	  -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.log' -o -name '*.glob' \
@@ -649,7 +650,7 @@ misc: $(patsubst %.sh,%.log,$(wildcard misc/*.sh))
 misc/universes.log: misc/universes/all_stdlib.v
 
 misc/universes/all_stdlib.v:
-	cd .. && $(MAKE) test-suite/$@
+	cd misc/universes && ./build_all_stdlib.sh > all_stdlib.v
 
 $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG)
 	@echo "TEST      $<"
-- 
cgit v1.2.3