aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rwxr-xr-xdev/ci/azure-build.sh1
-rw-r--r--dev/ci/user-overlays/13537-ppedrot-lazy-subst-kernel.sh5
2 files changed, 6 insertions, 0 deletions
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
diff --git a/dev/ci/user-overlays/13537-ppedrot-lazy-subst-kernel.sh b/dev/ci/user-overlays/13537-ppedrot-lazy-subst-kernel.sh
new file mode 100644
index 0000000000..aa686ea619
--- /dev/null
+++ b/dev/ci/user-overlays/13537-ppedrot-lazy-subst-kernel.sh
@@ -0,0 +1,5 @@
+if [ "$CI_PULL_REQUEST" = "13537" ] || [ "$CI_BRANCH" = "lazy-subst-kernel" ]; then
+
+ overlay mtac2 https://github.com/ppedrot/Mtac2 lazy-subst-kernel
+
+fi