From 11588869d33e7faba70ab29123e6fafedcd7def2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 17 Jul 2020 13:52:17 +0200
Subject: CI: Use bundled compcert for VST

---
 dev/ci/ci-vst.sh | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev')

diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 169d1a41db..4a332406a2 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -5,4 +5,6 @@ ci_dir="$(dirname "$0")"
 
 git_download vst
 
+export COMPCERT=bundled
+
 ( cd "${CI_BUILD_DIR}/vst" && make IGNORECOQVERSION=true )
-- 
cgit v1.2.3