From fa1e921257735d246d04be9e456f11ec7330b37a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 19 May 2017 13:17:08 +0200
Subject: Re-adding explicit dependency of misc universe test into
 all_stdlib.v.

Was working when calling test-suite from main Makefile but not when
calling directly from the test-suite Makefile.

The dependency was mistakenly dropped in 98a927aef.
---
 test-suite/Makefile | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'test-suite/Makefile')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 39ef05269..afaa48463 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -408,6 +408,11 @@ modules/%.vo: modules/%.v
 
 misc: $(patsubst %.sh,%.log,$(wildcard misc/*.sh))
 
+misc/universes.log: misc/universes/all_stdlib.v
+
+misc/universes/all_stdlib.v:
+	cd .. && $(MAKE) test-suite/$@
+
 $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG)
 	@echo "TEST      $<"
 	$(HIDE){ \
-- 
cgit v1.2.3