From 149b0c422027a31972b62457af1bf97bd016e26c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr>
Date: Sat, 27 May 2017 16:00:53 +0200
Subject: Gitlab CI

---
 test-suite/coq-makefile/template/init.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite/coq-makefile')

diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh
index bfd2c1b95..c952d41a3 100644
--- a/test-suite/coq-makefile/template/init.sh
+++ b/test-suite/coq-makefile/template/init.sh
@@ -1,5 +1,5 @@
 
-export PATH=../../../bin/:$PATH
+export PATH=$COQBIN:$PATH
 
 rm -rf theories src Makefile Makefile.conf tmp
 git clean -dfx || true
-- 
cgit v1.2.3