[gdb/tui] Don't include border_width in left_margin
authorTom de Vries <tdevries@suse.de>
Mon, 13 Nov 2023 20:22:50 +0000 (21:22 +0100)
committerTom de Vries <tdevries@suse.de>
Mon, 13 Nov 2023 20:22:50 +0000 (21:22 +0100)
commit5fa871f5d93bf285753f219cf583d0763dc0cd33
tree61a88157a6af44dcf5d15e09ab8e9d47489613c3
parentff3c86a844225a0f8848b2aee0b1628114c01377
[gdb/tui] Don't include border_width in left_margin

Currently left_margin does not match its documentation:
...
  /* Return the size of the left margin space, this is the space used to
     display things like breakpoint markers.  */
  int left_margin () const
  { return box_width () + TUI_EXECINFO_SIZE + extra_margin (); }
...

It is stated that the left margin is reserved to display things, but
the box_width is not used for that.

Fix this by dropping box_width () from the left_margin calculation.

Tested on x86_64-linux.

Approved-By: Tom Tromey <tom@tromey.com>
gdb/tui/tui-winsource.c
gdb/tui/tui-winsource.h