\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


Reply via email to