[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
them.
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.