\entry {\code {\xeatspaces {\char '15 }}}{13} Sigh. These kinds of index entries are so wrong, and so hard to eradicate.
I reverted my change. Oleg says he's working on the more complex fix. Thanks, karl
\entry {\code {\xeatspaces {\char '15 }}}{13} Sigh. These kinds of index entries are so wrong, and so hard to eradicate.
I reverted my change. Oleg says he's working on the more complex fix. Thanks, karl