Zsh Mailing List Archive
Messages sorted by: Reverse Date, Date, Thread, Author

Re: $PPID not updated when the PPID changes (parent killed)



On Wed, May 19, 2021, at 12:25 AM, Bart Schaefer wrote:
> So ... hopefully the attached patch addresses the assorted issues raised.
> 
> Attachments:
> * PPID.txt

Anyone else have feedback on this (48888), or is it ready to go?

-- 
vq




Messages sorted by: Reverse Date, Date, Thread, Author