aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xdev/ci/ci-bedrock2.sh2
-rwxr-xr-xdev/ci/ci-paramcoq.sh2
2 files changed, 2 insertions, 2 deletions
diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh
index 2ac78d3c2b..2d242d80a4 100755
--- a/dev/ci/ci-bedrock2.sh
+++ b/dev/ci/ci-bedrock2.sh
@@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")"
FORCE_GIT=1
git_download bedrock2
-( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make )
+( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make | iconv -t UTF-8 -c `#9767` )
diff --git a/dev/ci/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh
index c641af2abb..d2e0ee89bf 100755
--- a/dev/ci/ci-paramcoq.sh
+++ b/dev/ci/ci-paramcoq.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
git_download paramcoq
-( cd "${CI_BUILD_DIR}/paramcoq" && make && make install )
+( cd "${CI_BUILD_DIR}/paramcoq" && make && make install && cd test-suite && make examples)