diff options
| -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 + |