This is the mail archive of the gdb-patches@sources.redhat.com mailing list for the GDB project.

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

Re: [PATCH] Removal of markup annotations

> From: Nick Roberts <nickrob@snap.net.nz>
> Date: Wed, 22 Jun 2005 11:48:41 +1200
> Cc: gdb-patches@sources.redhat.com
> 
> 2005-06-22  Nick Roberts  <nickrob@snap.net.nz>
> 
> 	* gdb.texinfo (History) Rename "Command History".
> 	(Command History): Move node "Server Prefix" from section on
> 	Annotations here.

Fine with me, but please add indexing, so that this information could
be found quickly and efficiently.  At the very least, "@cindex
@code{server}, command prefix" should be there, and possibly also
something else, like perhaps "@cindex hide commands from history" or
some such (think about a user who'd wish to find the description of
the feature without knowing its exact name).
Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]