24 Jan
2019
24 Jan
'19
2:27 p.m.
My bug report's bug.sh script is broken. It needs "mpid=$!" before "sleep 0.5", and "wait $mpid" before "kill $pid".
--
Hallvard