[PATCH] gdb/configure.ac: add --enable-source-highlight

[Sergio Durigan Junior]

On Monday, March 18 2019, Eli Zaretskii wrote:

>> From: Sergio Durigan Junior <sergiodj@redhat.com>
>> Cc: Tom Tromey <tom@tromey.com>,  gdb-patches@sourceware.org
>> Date: Sun, 17 Mar 2019 23:52:51 -0400
>> 
>> Something Keith and I were talking about the other day is adding a
>> command line switch to enable/disable source highlight, so the user can
>> do:
>> 
>>   gdb --disable-source-highlight ...
>> 
>>   (or some such)
>
> We already have a variable, which you can set from your ~/.gdbinit,
> isn't that enough?

In my experience as a GDB user, it is.  But I'm thinking about people
who, for some reason, wouldn't like to keep (or don't know about) a
~/.gdbinit, and would like to disable the feature from the start.  It's
more convenient for the user to do:

  gdb --disable-source-highlight ...

  (The parameter could be named in a different, more concise way, of
  course)

than to do:

  echo 'set style source off' >> ~/.gdbinit
  gdb ...

or:

  gdb -ex 'set style source off' ...

  (IME, it's common for a user to not know about -ex)

But anyway, I don't want to bikeshed over this.  If it's a hard thing to
do, I'm totally fine with keeping things as is.

Thanks,

-- 
Sergio
GPG key ID: 237A 54B1 0287 28BF 00EF  31F4 D0EB 7628 65FC 5E36
Please send encrypted e-mail if possible
http://sergiodj.net/