[PATCH v2 3/7] Add "tips" file to gdb

[Simon Marchi]

On 2020-06-23 9:20 a.m., Tom Tromey wrote:
> This adds a "tips" file to gdb.  This file holds handy tips -- right
> now there are just a few, but it's easy to add more.  A random tip is
> displayed during interactive startup.

Awesome!  I propose we merge this after the GDB 11 branch creation, since
it would be a bit silly to ship this with only these three tips.  That will
give us time until the next release to add more.  I'll come up with some and
ask my colleagues who use GDB if they would have any ideas for some.

Simon