Hello all,

I am missing the $$ special variable to denote the current shell's pid (see http://hyperpolyglot.org/unix-shells giving a nice table ...); has it been discussed and rejected? What files should I look in to consider adding it?