Subject: Re: bug#42160: Issue with Man-kill and background process.
From: Eli Zaretskii <[email-masked]>
To: [email-masked]
Cc: [email-masked]
Date: Sat, 25 Jul 2020 10:16:38 +0300
List-Id: <debbugs-submit.debbugs.gnu.org>

> Date: Sat, 18 Jul 2020 10:46:07 +0300
> From: Eli Zaretskii <[email-masked]>
> Cc: [email-masked]
> 
> Ping! Ping!
> 
> Jimmy, could you please try this patch and see if it fixes your
> problems?  If it does, I' d like to install it.

No comments, so I installed the changes, and I'm closing this bug
report.