Re: [PATCH] DejaGnu kills the wrong process due to PID-reuse races

Pedro Alves <[email protected]> Wed, 29 Jul 2015 09:47:00 +0100

Newsgroups	gmane.comp.sysutils.dejagnu.general
Message-ID	<[email protected]>

On 07/29/2015 09:43 AM, Andreas Schwab wrote:
> Pedro Alves <[email protected]> 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