From 48ae6cec009554a337f64b0402daea2c653e25e2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 27 Nov 2018 10:56:09 +0100
Subject: Add a CI job running test suite with `-async-proofs on`

---
 .gitlab-ci.yml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index f54f64bf28..c11ba11fc5 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -151,7 +151,7 @@ after_script:
     - BIN=$(readlink -f ../_install_ci/bin)/
     - LIB=$(readlink -f ../_install_ci/lib/coq)/
     - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH"
-    - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" all
+    - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" COQFLAGS="${COQFLAGS}" all
   artifacts:
     name: "$CI_JOB_NAME.logs"
     when: on_failure
@@ -427,6 +427,13 @@ test-suite:edge+trunk+dune:
     expire_in: 1 week
   allow_failure: true
 
+test-suite:base+async:
+  <<: *test-suite-template
+  dependencies:
+    - build:base
+  variables:
+    COQFLAGS: "-async-proofs on"
+
 validate:base:
   <<: *validate-template
   dependencies:
-- 
cgit v1.2.3