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

[Pedro Alves]

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