From 765392492df2f5e065b2b5e706b6620846337cc0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 21 Sep 2017 00:53:10 +0200
Subject: Universe binders survive sections, modules and compilation.

---
 test-suite/Makefile | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'test-suite/Makefile')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index f169f86e88..6865dcc768 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -95,7 +95,8 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile
 
 PREREQUISITELOG = prerequisite/admit.v.log			\
-  prerequisite/make_local.v.log prerequisite/make_notation.v.log
+  prerequisite/make_local.v.log prerequisite/make_notation.v.log \
+  prerequisite/bind_univs.v.log
 
 #######################################################################
 # Phony targets
-- 
cgit v1.2.3