diff options
| author | Ben Gamari <ben@smart-cactus.org> | 2021-09-24 23:10:06 -0400 |
|---|---|---|
| committer | Ben Gamari <ben@smart-cactus.org> | 2021-09-24 23:14:31 -0400 |
| commit | 4b7ba3ae671ebd70fa7bdf744d30b8061db13016 (patch) | |
| tree | e72d3c4ea0ea8b1c70c003ac040a0a1988bf2714 /.gitlab/ci.sh | |
| parent | 33eb4a4e396e76cf8122a97734d0e8cdd850c747 (diff) | |
| download | haskell-4b7ba3ae671ebd70fa7bdf744d30b8061db13016.tar.gz | |
gitlab-ci: Don't rely on $HOME when pushing test metrics
As of cbfc0e933660626c9f4eaf5480076b6fcd31dceb we set $HOME to a
non-existent directory to ensure hermeticity.
Diffstat (limited to '.gitlab/ci.sh')
| -rwxr-xr-x | .gitlab/ci.sh | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/.gitlab/ci.sh b/.gitlab/ci.sh index c68d847135..d397d4de40 100755 --- a/.gitlab/ci.sh +++ b/.gitlab/ci.sh @@ -423,7 +423,12 @@ function push_perf_notes() { fi info "Pushing perf notes..." - "$TOP/.gitlab/test-metrics.sh" push + + # N.B. $HOME may be unset (e.g. is HERMETIC is set) yet test-metrics.sh + # relies on it for SSH configuration. Provide a temporary $HOME instead. + TMP_HOME="$(pwd)/.home" + HOME="$TMP_HOME" "$TOP/.gitlab/test-metrics.sh" push + rm -R "$TMP_HOME" } # Figure out which commit should be used by the testsuite driver as a |