source-academy / js-slang / 35717384304

86%

push

github

fix: kill the ssh-agent between the two deploy-docs deploy steps (#2093)

The /javascript and root deploy steps each invoke
peaceiris/actions-gh-pages, which starts an ssh-agent on a fixed
socket path (/tmp/ssh-auth.sock) and leaves it running. The second
step's own ssh-agent then fails to bind to that same path
("Address already in use"), as seen in the first run after #2092
merged: the /javascript deploy succeeded but the root deploy failed
outright.

Verified locally that `ssh-agent -k` (using the $SSH_AUTH_SOCK/
$SSH_AGENT_PID the first step already exported to the job
environment) correctly kills the agent and releases the socket, and
that a subsequent bind to the same path then succeeds.

Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>

2517 of 3052 branches covered (82.47%)

Branch coverage included in aggregate %.

4915 of 5622 relevant lines covered (87.42%)

446268.04 hits per line