Re: Variable pitch mode line

[Lars Ingebrigtsen]

Po Lu <luangruo@yahoo.com> writes:

> It seems a bit scary to me.  For example, how would I quickly find "see
> Optimize Options", if that was generated by a pxref, where the "see" and
> "Optimize Options" are in different nodes?

We don't have code for that today, but it doesn't seem particularly
difficult to implement.

-- 
(domestic pets only, the antidote for overdose, milk.)
   bloggy blog: http://lars.ingebrigtsen.no