aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-17 10:22:49 +0000
committerGitHub2020-11-17 10:22:49 +0000
commit81ff5b8b3033edb97e51c00a73878745fed4ddcb (patch)
treeaaac705195d93b06e69488b223e8b646b953a488
parent04b25a7635e796ad05ef7db537883594a5144a56 (diff)
parent7c6ebabaa48a427244acd748ffa784f192b1bd4d (diff)
Merge PR #13402: [ci] Use lite target for Perennial
Reviewed-by: SkySkimmer
-rwxr-xr-xdev/ci/ci-perennial.sh5
1 files changed, 1 insertions, 4 deletions
diff --git a/dev/ci/ci-perennial.sh b/dev/ci/ci-perennial.sh
index f3be66e814..306cbdf63c 100755
--- a/dev/ci/ci-perennial.sh
+++ b/dev/ci/ci-perennial.sh
@@ -6,7 +6,4 @@ ci_dir="$(dirname "$0")"
FORCE_GIT=1
git_download perennial
-# required by Perennial's coqc.py build wrapper
-export LC_ALL=C.UTF-8
-
-( cd "${CI_BUILD_DIR}/perennial" && git submodule update --init --recursive && make TIMED=false )
+( cd "${CI_BUILD_DIR}/perennial" && git submodule update --init --recursive && make TIMED=false lite )