Commit 20c554e6 authored by Ralf Jung's avatar Ralf Jung
Browse files

Revert "silence "no common root" warning"

This reverts commit c5ff6a3e.
It did not work (needs to be set as a coq_makefile option) so I moved the flag to the _CoqProject file instead.
parent c5ff6a3e
......@@ -51,7 +51,6 @@ fi
if [[ "$CI_RUNNER_DESCRIPTION" == "coop-timing" ]]; then
export TIMECMD=ci/perf
# git-ignore CI-generated files
mkdir -p .git/info
cat >> .git/info/exclude <<EOF
......@@ -64,7 +63,6 @@ EOF
# Build
status "[buildjob] Perfoming build (make $MAKE_TARGET)"
export INSTALLDEFAULTROOT=ci # silence "no common root" warning
time make --output-sync --no-print-directory -k -j$CPU_CORES $MAKE_TARGET 2>&1 | tee build-log.txt
# Check for warnings
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment