Use SIGKILL to actually kill the runner

pull/7045/head
Juliusz Sosinowicz 2023-12-08 16:27:10 +01:00
parent 21381b939b
commit 1bf0d8c896
2 changed files with 6 additions and 6 deletions

View File

@ -1,14 +1,14 @@
#!/bin/sh #!/bin/sh
if [ -z "$GITHUB_WORKSPACE" ]; then if [ -z "$GITHUB_WORKSPACE" ]; then
echo '$GITHUB_WORKSPACE is not set' echo '$GITHUB_WORKSPACE is not set'
exit 1 exit 1
fi fi
if [ -z "$HOST_ROOT" ]; then if [ -z "$HOST_ROOT" ]; then
echo '$HOST_ROOT is not set' echo '$HOST_ROOT is not set'
exit 1 exit 1
fi fi
chroot $HOST_ROOT make -C $GITHUB_WORKSPACE/memcached \ chroot $HOST_ROOT make -C $GITHUB_WORKSPACE/memcached \
-j$(nproc) PARALLEL=$(nproc) test_tls -j$(nproc) PARALLEL=$(nproc) test_tls

View File

@ -90,7 +90,7 @@ jobs:
MEMCACHED_RES=0 # Not set when command succeeds MEMCACHED_RES=0 # Not set when command succeeds
# Tests should usually take less than 4 minutes. If already taking # Tests should usually take less than 4 minutes. If already taking
# 5 minutes then they are probably stuck. Interrupt and re-run. # 5 minutes then they are probably stuck. Interrupt and re-run.
timeout 5m docker run -v /:/host \ time timeout -s SIGKILL 5m docker run -v /:/host \
-v $GITHUB_WORKSPACE/build-dir/bin/memcached.sh:/memcached.sh \ -v $GITHUB_WORKSPACE/build-dir/bin/memcached.sh:/memcached.sh \
-e GITHUB_WORKSPACE=$GITHUB_WORKSPACE \ -e GITHUB_WORKSPACE=$GITHUB_WORKSPACE \
-e HOST_ROOT=/host \ -e HOST_ROOT=/host \