> Texinfo has a command @backslashchar{} that produces a backslash,
> but I don't know if it works with texi2html. If it does, you could
> do @warning{@backslashchar{}command} instead.
For the record, we are involuntarily married to the ancient texi2html
version 1.82, which doesn't support `@backslashchar`.
Werner
