From b481ae12fb55cc558d58b9902f1020e43f76fc4e Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 7 Dec 2020 11:22:17 +0100
Subject: Move Azure jobs to GitHub Actions.

---
 dev/ci/azure-build.sh | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev/ci')

diff --git a/dev/ci/azure-build.sh b/dev/ci/azure-build.sh
index 494651c5bf..1b02cd45ed 100755
--- a/dev/ci/azure-build.sh
+++ b/dev/ci/azure-build.sh
@@ -4,4 +4,5 @@ set -e -x
 
 cd $(dirname $0)/../..
 
+eval $(opam env)
 dune build coq.install coqide-server.install
-- 
cgit v1.2.3