From 741943da6e42937f6d50db9c920a40073160eebc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 16 Aug 2017 22:28:26 +0200
Subject: Fix GitLab CI

- timing needs time and python

- check for compiled files without source looks in the install
  directory (except for make -f Makefile.ci which doesn't check), as
  such the install directory has been renamed to _install_ci and isn't
  searched.
---
 dev/ci/ci-common.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 238960948d..358f527f9e 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -4,7 +4,7 @@ set -xe
 
 if [ -n "${GITLAB_CI}" ];
 then
-    export COQBIN=`pwd`/install/bin
+    export COQBIN=`pwd`/_install_ci/bin
 else
     export COQBIN=`pwd`/bin
 fi
-- 
cgit v1.2.3