fix configuring git exclude

0e0b707d · Ralf Jung · 7e7a41e0 · 0e0b707d
Commit 0e0b707d authored Aug 28, 2020 by Ralf Jung
--- a/buildjob
+++ b/buildjob
@@ -51,7 +51,7 @@ if [[ "$CI_RUNNER_DESCRIPTION" == "coop-timing" ]]; then
 fi
 # git-ignore CI-generated files
 mkdir -p .git/info
-echo >> .git/info/exclude <<EOF
+cat >> .git/info/exclude <<EOF
 ci/
 opamroot/
 build-env.txt