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

[Vincent Lefevre <vincent@vinc17.net>]

Consider the following script:

#!/usr/bin/env zsh
echo $ZSH_VERSION
f() { grep PPid /proc/$$/status; echo $PPID }
f
kill -9 $PPID
sleep 1
f

Under Linux, I get:

zira% sh -c ./tst.zsh; sleep 2
5.8
PPid:   39867
39867
zsh: killed     sh -c ./tst.zsh
PPid:   1
39867
zira% 

i.e. $PPID is not updated when the PPID changes, i.e. the parent
process is killed.

The zshparam(1) man page says:

  PPID <S>
      The process ID of the parent of the shell.  As for $$, the value
      indicates the parent of the original shell and does  not  change
      in subshells.

This implies that it should be updated when the process ID of the
parent of the shell changes.

-- 
Vincent Lefèvre <vincent@vinc17.net> - Web: <https://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <https://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)