fix: Store pid for serial debugging (#1288)

This commit is contained in:
Kroese
2026-07-17 14:44:49 +02:00
committed by GitHub
parent 585ebb3f53
commit 5c889b272d
+11 -4
View File
@@ -52,11 +52,18 @@ buildHostArguments() {
startHostBinary() {
local pid=""
if enabled "$HOST_DEBUG"; then
set -x
./host.bin "${HOST_ARGS[@]}" &
{ set +x; } 2>/dev/null
echo "$!" > "$HOST_PID"
{
set -x
./host.bin "${HOST_ARGS[@]}" &
pid=$!
{ set +x; } 2>/dev/null
} 2>&1
echo "$pid" > "$HOST_PID"
echo
else
./host.bin "${HOST_ARGS[@]}" >/dev/null &