Re: [PATCH] git-gui: remove lines starting with the comment character

From: Johannes Sixt <j6t@kdbg.org>
Date: Feb 3, 2021, 21:42 UTC
Message-ID: <ba8baa8c-d308-c7c9-b15c-4582cc41863e@kdbg.org>
In-Reply-To: <CAPig+cQxASd8YNm+6E4XkiEoR__hAW8nrUbEkaBoJSicpq_rmA@mail.gmail.com>

Am 03.02.21 um 18:58 schrieb Eric Sunshine:

Show 19 quoted lines

> On Wed, Feb 3, 2021 at 12:48 PM Eric Sunshine <sunshine@sunshineco.com> wrote:
>> So, perhaps one way forward is for Pratyush to emulate that behavior
>> and insert some text into the edit box saying "lines beginning with
>> '#' will be ignored", or add a label above or below the edit box
>> stating the same. (Of course, the actual displayed comment-character
>> should be determined dynamically.)
> 
> Even more fancy would be to add a checkbox below the edit field which
> both enables/disables the "stripspace" behavior and allows the user to
> specify the comment-character. For instance:
> 
>     [x] ignore lines beginning with [#]
> 
> where [x] is the checkbox and [#] is a text field in which the user
> can type the comment-character.
> 
> For convenience, the checkbox would be checked by default, and the
> comment-character would default to the user's configured
> comment-character or "#".

While I'm not thrilled by this solution, it's probably the only sensible way forward. We would have to place the checkbox above the edit field, where there's still some space; otherwise, it takes away vertical space, and that I really prefer to use for the commit message and the patch text.

I don't think, though, that we need an edit field to change the comment character. It's a fairly stable setting, and as long as there's a preference for it and it's synchronized into the checkbox caption, it is fine, IMO.

-- Hannes