[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: tooltip custom group: duplicate labels

From: Richard M. Stallman
Subject: Re: tooltip custom group: duplicate labels
Date: Sun, 11 Dec 2005 11:49:36 -0500

    I suggest removing their tags to show unambiguous labels that have the
    word "tooltip".

I see no reason to keep any of the tags in gud.el.  Let's just delete

    Perhaps there should be some generic solution, e.g. using a heuristic
    to place an option with the substring "-mode" before other options in
    the customization buffer or something like this.

That might be a good idea; I will add it to etc/TODO.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]