Commit 7e7a41e0 authored by Ralf Jung's avatar Ralf Jung
Browse files

make sure the dir exists

parent 1853283c
...@@ -49,6 +49,8 @@ fi ...@@ -49,6 +49,8 @@ fi
if [[ "$CI_RUNNER_DESCRIPTION" == "coop-timing" ]]; then if [[ "$CI_RUNNER_DESCRIPTION" == "coop-timing" ]]; then
export TIMECMD=ci/perf export TIMECMD=ci/perf
fi fi
# git-ignore CI-generated files
mkdir -p .git/info
echo >> .git/info/exclude <<EOF echo >> .git/info/exclude <<EOF
ci/ ci/
opamroot/ opamroot/
......
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