From 2b33af7d4572122f585c8826e60fbe51db602551 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 5 Oct 2017 18:43:08 +0200
Subject: GitLab CI: make all_stdlib.v in build job

---
 .gitlab-ci.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index ae55302d11..d2e335d45a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -60,6 +60,7 @@ before_script:
     paths:
       - _install_ci
       - config/Makefile
+      - test-suite/misc/universes/all_stdlib.v
     expire_in: 1 week
   script:
     - set -e
@@ -70,6 +71,7 @@ before_script:
 
     - echo 'start:coq.build'
     - make -j ${NJOBS}
+    - make test-suite/misc/universes/all_stdlib.v
     - echo 'end:coq:build'
 
     - echo 'start:coq.install'
-- 
cgit v1.2.3