Should it push it?

Eli Zaretskii <eliz@gnu.org> writes:

>> From: Philip Kaludercic <philipk@posteo.net>
>> Cc: 55426@debbugs.gnu.org
>> Date: Sun, 15 May 2022 11:06:42 +0000
>> 
>> Thank you for your comments, here is an improved version:
>
> Thanks.  One nit:
>
>> +** Shell
>> +
>> +---
>> +*** New user option 'shell-kill-buffer-on-exit'
>> +Enabling this open will automatically kill a *shell* buffer as soon as
>                  ^^^^
> Seems like a leftover from a different version?

Andreas Schwab <schwab@linux-m68k.org> writes:

> On Mai 15 2022, Philip Kaludercic wrote:
>
>> diff --git a/lisp/shell.el b/lisp/shell.el
>> index 47887433d9..7000d38255 100644
>> --- a/lisp/shell.el
>> +++ b/lisp/shell.el
>> @@ -331,6 +331,12 @@ shell-has-auto-cd
>>    :group 'shell-directories
>>    :version "28.1")
>>  
>> +(defcustom shell-kill-buffer-on-exit t
>
> That should default to nil.