Commit 1853283c authored by Ralf Jung's avatar Ralf Jung
Browse files

gitignore CI-generated files

parent 295a6538
......@@ -49,6 +49,12 @@ fi
if [[ "$CI_RUNNER_DESCRIPTION" == "coop-timing" ]]; then
export TIMECMD=ci/perf
fi
echo >> .git/info/exclude <<EOF
ci/
opamroot/
build-env.txt
build-times.txt
EOF
# Build
status "[buildjob] Perfoming build (make $MAKE_TARGET)"
......
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