Merge PR coq#19375: Minor CI cleanup / fixes around elpi

Reviewed-by: gares Reviewed-by: proux01 Co-authored-by: proux01 <[email protected]>
Alizter · Jul 17, 2024 · bbfc24d · bbfc24d
2 parents c0f406b + 8e89d79
commit bbfc24d
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Makefile.ci b/Makefile.ci
@@ -148,8 +148,8 @@ ci-analysis: ci-elpi_hb ci-finmap ci-bigenough
 
 ci-hb: ci-elpi
 
-ci-elpi_test: ci-elpi_hb
-ci-hb_test: ci-elpi_hb
+ci-elpi_test: ci-elpi
+ci-hb_test: ci-hb
 
 ci-trakt: ci-elpi
 

diff --git a/dev/ci/ci-elpi_test.sh b/dev/ci/ci-elpi_test.sh
@@ -8,7 +8,7 @@ ci_dir="$(dirname "$0")"
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
 ( cd "${CI_BUILD_DIR}/elpi"
-  export DUNE_build_FLAGS="--root ."
+  export DUNE_build_FLAGS="--release"
   make test-core
   make examples
   make test-apps