Re: Another doc patch: setkey

[Alessandro Rubini]

> It may make the DVI more readable, but it makes the Info worse.  Using
> address@hidden' produces `SOME-NAME' under Info,

Yes, I've seen it. An option os using no marker at all, leaving the
names in roman in the dvi version.  I think list entry like it is now
looks very unprofessional (both for the excessive courier in the
inline list and in the page-and-a-halt wasted in the subsequent list.

I agree that it is a detail, and subject to personal judjment, but
that entry gives a very bad impression when one prints the docs.

It's up to you, anyways.

/alessandro