aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorSamuel Gruetter2019-02-09 19:30:15 -0500
committerSamuel Gruetter2019-02-09 19:30:15 -0500
commit39075d0d1d6da98f32782f64ca34f326bdca57a1 (patch)
tree48874abf65a13992a216d65be1030454acb4d592 /dev
parent727f2b18606bf88a744aec2ba2a594312f7f5833 (diff)
remove VERBOSE=1, gitlab log shows that `-async-proofs-tac-j 1` was indeed passed
https://gitlab.com/coq/coq/-/jobs/158737429
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/ci-bedrock2.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh
index f901109141..2ac78d3c2b 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"' VERBOSE=1 make )
+( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make )