From bb070732dfb3ad06f90c47d1010970faee0c195e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 23 Nov 2017 15:12:33 +0100
Subject: Make byte on gitlab.

Hopefully this will stop the intermittent
test-suite/coq-makefile/findlib-package failures.
---
 .gitlab-ci.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7c3489de4..c0a01f3fd 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -71,12 +71,14 @@ before_script:
     - echo 'end:coq.config'
 
     - echo 'start:coq.build'
+    - make -j ${NJOBS} byte
     - make -j ${NJOBS}
     - make test-suite/misc/universes/all_stdlib.v
     - echo 'end:coq:build'
 
     - echo 'start:coq.install'
     - make install
+    - make install-byte
     - cp bin/fake_ide _install_ci/bin/
     - echo 'end:coq.install'
 
-- 
cgit v1.2.3