diff options
| author | Ben Gamari <ben@smart-cactus.org> | 2020-07-23 14:07:39 -0400 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-07-26 13:23:59 -0400 |
| commit | 9cbfe0868418a531da0872b0c477a15aa67f8861 (patch) | |
| tree | 15ab5451155700756759de07ef747b3ac97db8f6 /.gitlab | |
| parent | e91672f0b7185bbafbe8ed1f2ae2cb775111f950 (diff) | |
| download | haskell-9cbfe0868418a531da0872b0c477a15aa67f8861.tar.gz | |
gitlab-ci: Kill ssh-agent after pushing test metrics
Otherwise the Windows builds hang forever waiting for the process to
terminate.
Diffstat (limited to '.gitlab')
| -rwxr-xr-x | .gitlab/test-metrics.sh | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/.gitlab/test-metrics.sh b/.gitlab/test-metrics.sh index 75952d28de..5ffb8110d9 100755 --- a/.gitlab/test-metrics.sh +++ b/.gitlab/test-metrics.sh @@ -81,6 +81,10 @@ function push() { echo "" echo "Failed to push git notes. Fetching, appending, and retrying... $MAX_RETRY retries left." done + + # Be sure to kill agent before we terminate since otherwise the Windows CI + # job won't finish. + ssh-agent -k } case $1 in @@ -88,3 +92,4 @@ case $1 in pull) pull ;; *) fail "Invalid mode $1" ;; esac + |