% characters through. By default, we re-enable |\|, and make `\verb*" "'
% typeset some space glue, rather than a space character. A macro
% `\verb*"\ "' is defined to actually print a space character, which yield
% characters through. By default, we re-enable |\|, and make `\verb*" "'
% typeset some space glue, rather than a space character. A macro
% `\verb*"\ "' is defined to actually print a space character, which yield