|
From: | Pedro Alves |
Subject: | Re: [PATCH] DejaGnu kills the wrong process due to PID-reuse races |
Date: | Wed, 29 Jul 2015 09:47:00 +0100 |
User-agent: | Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.5.0 |
On 07/29/2015 09:43 AM, Andreas Schwab wrote: > Pedro Alves <address@hidden> writes: > >> + # Prepend "-" to generate the "process group ID" needed by >> + # kill. >> + set pgid "-[join $pid { -}]" > > That's an odd way to write [expr -$pid]. Indeed. I just copied it here from local_exec without thinking about it. Do we even need [expr]? I'd think: set pgid "-$pid" would work just as well. Thanks, Pedro Alves
[Prev in Thread] | Current Thread | [Next in Thread] |