On 2019-07-18 14:53, Richard Hector wrote:
On 18/07/19 1:29 PM, John Crawley wrote:However, try running in a terminal: echo $$ exec <someterminal> #Then, in the new terminal: echo $$ The two PIDs are different! (or were here)Yes. You exec'd a terminal, which then started a shell. You'll probably find (I did) that the first pid you got is now the pid of the terminal:
Ah, that makes sense. Thanks. -- John