use absolute path for TIMECMD

82035bb9 · Ralf Jung · 8abf93d7 · 82035bb9
Commit 82035bb9 authored Sep 30, 2020 by Ralf Jung
--- a/buildjob
+++ b/buildjob
@@ -49,7 +49,7 @@ if [[ -n "$MANGLE_NAMES" ]]; then
    export COQEXTRAFLAGS="$COQEXTRAFLAGS -mangle-names _"
 fi
 if [[ "$CI_RUNNER_DESCRIPTION" == "coop-timing" ]]; then
-    export TIMECMD=ci/perf
+    export TIMECMD=$PWD/ci/perf
 fi
 # git-ignore CI-generated files (some projects look at `git status` in their CI)
 mkdir -p .git/info